B-метод
Метод B — это метод разработки программного обеспечения, основанный на B с инструментальной поддержкой , формальном методе , основанном на абстрактной машинной нотации , используемом при разработке компьютерного программного обеспечения . [1] [2]
Обзор [ править ]
B был первоначально разработан в 1980-х годах Жаном-Раймоном Абриалем. [3] [4] во Франции и Великобритании . B связан с нотацией Z (также разработанной Abrial) и поддерживает разработку кода языка программирования на основе спецификаций. B использовался в основных системах, критически важных для безопасности , в Европе (таких как автоматические линии 14 и 1 парижского метро и ракета Ariane 5 ). [5] [6] [7] Он имеет надежные коммерчески доступные инструменты для спецификации , проектирования , проверки и генерации кода .
По сравнению с Z, B немного более низкоуровневый и больше ориентирован на уточнение кода, а не просто на формальную спецификацию — следовательно, легче правильно реализовать спецификацию, написанную на B, чем на Z. В частности, существует хорошая инструментальная поддержка для этот.Один и тот же язык используется в спецификациях, проектировании и программировании.Механизмы включают инкапсуляцию и локальность данных.
Событие-Б [ править ]
Впоследствии появился еще один формальный метод под названием Event-B. [8] [9] [10] был разработан на основе B-метода при поддержке платформы Rodin . [11] [12] Event-B — формальный метод, направленный на моделирование и анализ на уровне системы. Особенностями Event-B являются использование теории множеств для моделирования, использование уточнения для представления систем на разных уровнях абстракции и использование математических доказательств для проверки согласованности между этими уровнями уточнения.
Основные компоненты [ править ]
Обозначение B зависит от теории множеств и логики первого порядка и позволяет указать различные версии программного обеспечения, охватывающие полный цикл разработки проекта.
Абстрактная машина [ править ]
В первой и самой абстрактной версии, которая называется «Абстрактная машина» , дизайнер должен указать цель дизайна.
Уточнение [ править ]
- Затем, на этапе уточнения, они могут дополнить спецификацию, чтобы уточнить цель или сделать абстрактную машину более конкретной, добавив подробности о структурах данных и алгоритмах, которые определяют, как достигается цель.
- Новая версия, которая называется Refinement , должна быть согласованной и включать все свойства абстрактной машины.
- Проектировщик может использовать библиотеки B для моделирования структур данных или для включения или импорта существующих компонентов.
Реализация [ править ]
- Уточнение продолжается до тех пор, пока не будет достигнута детерминированная версия: Реализация .
- На всех этапах разработки используется одна и та же нотация, и последняя версия может быть переведена на язык программирования для компиляции.
Программное обеспечение [ править ]
B-Toolkit [ править ]
Инструментарий B- [13] [14] представляет собой набор инструментов программирования, предназначенных для поддержки использования B-Tool, [15] — это математический интерпретатор, основанный на теории множеств, предназначенный для поддержки B-метода. Первоначально разработкой занимались Иб Холм Соренсен и другие в компании BP Research, а затем в B-Core (UK) Limited. [16]
Инструментарий использует собственный X Window Motif . интерфейс [17] для управления графическим интерфейсом и работает в основном в операционных системах Linux , Mac OS X и Solaris .
Исходный код B-Toolkit теперь доступен. [18]
Ателье Б [ править ]
Разработано ClearSy, Atelier B [19] [20] представляет собой промышленный инструмент, позволяющий оперативно использовать метод Б для разработки бездефектного проверенного программного обеспечения (формального программного обеспечения). Доступны две версии: 1) Community Edition доступна каждому без каких-либо ограничений; 2) Версия Maintenance Edition только для держателей контрактов на техническое обслуживание. Atelier B использовалось для разработки автоматики безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens , а также для сертификации по общим критериям и разработки системных моделей компаниями ATMEL и STMicroelectronics .
Rodin[editРоден
Платформа Rodin — это инструмент, поддерживающий Event-B . [8] [21] [11] Rodin основан на программной среде IDE Eclipse ( интегрированной среде разработки ) и обеспечивает поддержку уточнений и математических доказательств . Платформа имеет открытый исходный код и является частью платформы Eclipse. Ее можно расширять с помощью подключаемых модулей программных компонентов . Развитие Rodin поддерживается проектами Европейского Союза DEPLOY (2008–2012 гг.), RODIN (2004–2007 гг.) и ADVANCE (2011–2014 гг.). [8]
БХДЛ [ править ]
BHDL предоставляет метод правильного проектирования цифровых схем , сочетающий в себепреимущества языка описания аппаратуры VHDL с формальностью Б. [22]
APCB [ править ]
APCB ( по-французски : Association de Pilotage des Conférences B , Руководящий комитет Международной конференции B ) организовал встречи, связанные с B-методом. [23] Он организовал конференции ZB с группой пользователей Z и конференции ABZ, включая абстрактные конечные автоматы а также нотацию Z. (ASM) ,
Книги [ править ]
- Книга B: присвоение программ значениям , Жан-Раймон Абриаль , издательство Кембриджского университета , 1996. ISBN 0-521-49619-5 .
- B-Метод: Введение , Стив Шнайдер, Пэлгрейв Макмиллан , серия «Краеугольные камни вычислений», 2001. ISBN 0-333-79284-X .
- Разработка программного обеспечения с B , Джоном Вордсвортом, Эддисоном Уэсли Лонгманом , 1996. ISBN 0-201-40356-0 .
- Язык и метод B: Руководство по практическому формальному развитию , Кевин Лано , Springer-Verlag , серия FACIT, 1996. ISBN 3-540-76033-4 .
- Спецификация в B: Введение с использованием B Toolkit , Кевин Лано , World Scientific Publishing Company , Imperial College Press , 1996. ISBN 1-86094-008-0 .
- Моделирование в Event-B: системная и программная инженерия , Жан-Раймон Абриаль , Cambridge University Press , 2010. ISBN 978-0-521-89556-9 .
Конференции [ править ]
Следующие конференции явно включали B-метод и/или событие-B:
- Конференция Z2B, Нант , Франция , 10–12 октября 1995 г.
- Первая конференция B, Нант, Франция, 25–27 ноября 1996 г.
- Вторая конференция B, Монпелье , Франция, 22–24 апреля 1998 г.
- ZB 2000, Йорк , Великобритания , 28 августа – 2 сентября 2000 г.
- ZB 2002, Гренобль , Франция, 23–25 января 2002 г.
- ZB 2003, Турку , Финляндия , 4–6 июня 2003 г.
- ZB 2005, Гилфорд , Великобритания, 2005 г.
- B 2007, Безансон , Франция, 2007 г.
- B, от исследований к преподаванию, Нант, Франция, 16 июня 2008 г.
- B, от исследований к преподаванию, Нант, Франция, 8 июня 2009 г.
- B, от исследований к преподаванию, Нант, Франция, 7 июня 2010 г.
- ABZ 2008, Британское компьютерное общество , Лондон , Великобритания, 16–18 сентября 2008 г.
- ABZ 2010, Орфорд , Квебек , Канада , 23–25 февраля 2010 г.
- ABZ 2012, Pisa , Italy , 18–22 June 2012
- ABZ 2014, Тулуза , Франция, 2–6 июня 2014 г.
- ABZ 2016, Линц , Австрия , 23–27 мая 2016 г.
- ABZ 2018, Саутгемптон , Великобритания, 2018 г.
- ABZ 2020, Ульм , Германия , 2021 г. (отложено из-за пандемии COVID-19 )
- ABZ 2021, Ульм, Германия, 2021 г.
См. также [ править ]
Ссылки [ править ]
- ^ Канселл, Доминик и Доминик Мери. «Основы метода Б». Вычислительная техника и информатика 22, вып. 3–4 (2003): 221–256.
- ^ Батлер, Майкл, Филипп Кернер, Себастьян Крингс, Тьерри Леконт, Майкл Леушель, Луис-Фернандо Мехиа и Лоран Вуазен. «Первые двадцать пять лет промышленного использования Б-метода». На Международной конференции по формальным методам для промышленных критических систем, стр. 189-209. Спрингер , Чам, 2020 г.
- ^ Жан-Раймон Абриаль (1988). «Инструмент B (Аннотация)» (PDF) . В Блумфилде, Робин Э.; Маршалл, Линн С.; Джонс, Роджер Б. (ред.). ВДМ – Путь вперед, Учеб. 2-й симпозиум VDM-Европа . Конспекты лекций по информатике . Том. 328. Спрингер. стр. 86–87. дои : 10.1007/3-540-50214-9_8 . ISBN 978-3-540-50214-2 .
- ^ Абриал-младший, Мэтью К.О. Ли, Д.С. Нейлсон, П.Н. Шарбах и Иб Холм Соренсен. «Б-метод». На Международном симпозиуме VDM Europe, стр. 398-405. Шпрингер, Берлин, Гейдельберг, 1991.
- ^ Герхарт, Сьюзен, Д. Крейген и Тед Ралстон. «Пример: система сигнализации парижского метро». Программное обеспечение IEEE 11, вып. 1 (1994): 32–28.
- ^ Бем, Патрик, Поль Бенуа, Ален Февр и Жан-Марк Мейнадье. «МЕТЕОР: успешное применение Б в большом проекте». На Международном симпозиуме по формальным методам, стр. 369–387. Шпрингер, Берлин, Гейдельберг, 1999.
- ^ Леконт, Тьерри. «Применение формального метода в промышленности: 15-летняя траектория». На Международном семинаре по формальным методам для промышленных критических систем, стр. 26-34. Шпрингер, Берлин, Гейдельберг, 2009 г.
- ^ Jump up to: Перейти обратно: а б с «Событие-Б и платформа Родена» . Event-B.org .
- ^ Батлер, Майкл. «Структуры декомпозиции для События-Б». На Международной конференции по интегрированным формальным методам, стр. 20–38. Шпрингер, Берлин, Гейдельберг, 2009 г.
- ^ Абриаль, Жан-Раймон. Моделирование в Event-B: системная и программная инженерия. Издательство Кембриджского университета , 2010.
- ^ Jump up to: Перейти обратно: а б Абриал, Жан-Раймонд, Майкл Батлер, Стефан Халлерстеде, Тай Сон Хоанг, Фархад Мехта и Лоран Вуазен. «Rodin: открытый набор инструментов для моделирования и рассуждений в Event-B». Международный журнал по программным инструментам для трансфера технологий 12, вып. 6 (2010): 447-466.
- ^ Хоанг, Тай Сон, Андреас Фюрст и Жан-Раймон Абриал. «Шаблоны Event-B и их инструментальная поддержка». Программное обеспечение и моделирование систем 12, вып. 2 (2013): 229–244.
- ^ «Набор инструментов B» . [B-Core (UK) Limited] . 2004. Архивировано из оригинала 12 октября 2004 года . Проверено 22 февраля 2012 г.
- ^ Хотон, Ховард и Кевин Лано. Спецификация в B: введение в использование инструментария B. Всемирный научный, 1996.
- ^ Абриаль, Жан-Раймон. «Инструмент Б». На Международном симпозиуме VDM Europe, стр. 86-87. Шпрингер, Берлин, Гейдельберг, 1988.
- ^ Боуэн, Джонатан (июль 2022 г.). «Иб Холм Соренсен: десять лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 41–49 . Проверено 3 августа 2022 г.
- ^ Требования к B-Toolkit , заархивировано 12 октября 2004 г. на Wayback Machine.
- ^ Крайтон, Эдвард. «Исходный код B-Toolkit» . Гитхаб .
- ^ «АтельеБ.еу» .
- ^ Ментре, Давид, Клод Марше, Жан-Кристоф Филлиатр и Масаси Аска. «Выполнение обязательств по доказательству от Ателье Б с использованием нескольких автоматических проверочных устройств». На Международной конференции по абстрактным государственным машинам, сплавам, B, VDM и Z, стр. 238-251. Шпрингер, Берлин, Гейдельберг, 2012 г.
- ^ Абриал, младший. «Процесс разработки системы с использованием Event-B и платформы Rodin». На Международной конференции по формальным инженерным методам, стр. 1-3. Шпрингер, Берлин, Гейдельберг, 2007 г.
- ^ Алджер, Аммар, Филипп Девьен, Софи Тайсон, JL. Буланже и Жорж Мариано. «BHDL: Схемотехника в B». На Третьей международной конференции по применению параллелизма в проектировании систем, 2003. Труды, стр. 241-242. ИИЭР, 2003.
- ^ «Ассоциация управления конференциями B» . книжный магазинcosmopolite.com . Проверено 27 июля 2022 г.
Внешние ссылки [ править ]
- B Method.com - работы и предметы, касающиеся метода B, формального метода с доказательством.
- Atelier B.eu. Архивировано 21 февраля 2008 г. в Wayback Machine : Atelier B — это мастерская системного проектирования, которая позволяет разрабатывать программное обеспечение, гарантированно безупречное.
- Зона Б Гренобль
| Базы данных органов управления : Национальные |
|---|
