B-метод

Метод разработки программного обеспечения

Метод B — это метод разработки программного обеспечения , основанный на B , формальном методе с инструментальной поддержкой , основанном на абстрактной машинной нотации , используемом при разработке компьютерного программного обеспечения . ^{[1] [2]}

Обзор

Первоначально B был разработан в 1980-х годах Жаном-Раймоном Абриалем ^{[3] [4]} во Франции и Великобритании . B связан с нотацией Z (также разработанной Abrial) и поддерживает разработку кода языка программирования на основе спецификаций. B использовался в основных системах, критически важных для безопасности, в Европе (таких как автоматические линии 14 и 1 парижского метро и ракета Ariane 5 ). ^{[5] [6] [7]} Он имеет надежные коммерчески доступные инструменты для спецификации , проектирования , проверки и генерации кода .

По сравнению с Z, B немного более низкоуровневый и больше ориентирован на уточнение кода, а не просто на формальную спецификацию — следовательно, легче правильно реализовать спецификацию, написанную на B, чем на Z. В частности, существует хорошая инструментальная поддержка для этот. Один и тот же язык используется в спецификациях, проектировании и программировании. Механизмы включают инкапсуляцию и локальность данных.

Событие-Б

Впоследствии на основе B-метода был разработан еще один формальный метод под названием Event-B ^{[8] [9] [10] , поддерживаемый Платформой Родена. [11] [12]} Event-B — формальный метод, направленный на моделирование и анализ на уровне системы. Особенностями Event-B являются использование теории множеств для моделирования, использование уточнения для представления систем на разных уровнях абстракции и использование математических доказательств для проверки согласованности между этими уровнями уточнения.

Основные компоненты

Обозначение B зависит от теории множеств и логики первого порядка и позволяет указать различные версии программного обеспечения, охватывающие полный цикл разработки проекта.

Абстрактная машина

В первой и самой абстрактной версии, которая называется « Абстрактная машина» , дизайнер должен указать цель дизайна.

Уточнение

• Затем, на этапе уточнения, они могут дополнить спецификацию, чтобы уточнить цель или сделать абстрактную машину более конкретной, добавив подробности о структурах данных и алгоритмах, которые определяют, как достигается цель.
• Новая версия, которая называется Refinement , должна быть согласованной и включать все свойства абстрактной машины.
• Проектировщик может использовать библиотеки B для моделирования структур данных или для включения или импорта существующих компонентов.

Выполнение

• Уточнение продолжается до тех пор, пока не будет достигнута детерминированная версия: Реализация .
• На всех этапах разработки используется одна и та же нотация, и последняя версия может быть переведена на язык программирования для компиляции.

Программное обеспечение

B-Инструментарий

B -Toolkit ^{[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]} представляет собой промышленный инструмент, позволяющий оперативно использовать метод B для разработки бездефектного проверенного программного обеспечения (формального программного обеспечения). Доступны две версии: 1) Community Edition доступна каждому без каких-либо ограничений; 2) Версия Maintenance Edition только для владельцев контрактов на техническое обслуживание. Atelier B использовалась для разработки автоматики безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens , а также для сертификации по общим критериям и разработки системных моделей компаниями ATMEL и STMicroelectronics .

Роден

Платформа Rodin — это инструмент, поддерживающий Event-B. ^{[8] [21] [11]} Rodin основан на программной среде IDE Eclipse ( интегрированной среде разработки ) и обеспечивает поддержку уточнений и математических доказательств . Платформа имеет открытый исходный код и является частью платформы Eclipse. Ее можно расширять с помощью подключаемых модулей программных компонентов . Развитие Rodin поддерживается проектами Европейского Союза DEPLOY (2008–2012), RODIN (2004–2007) и ADVANCE (2011–2014). ^[8]

БХДЛ

BHDL предоставляет метод правильного проектирования цифровых схем , сочетающий в себе преимущества языка описания аппаратуры VHDL с формальностью B. ^[22]

АПЦБ

APCB ( по-французски : Association de Pilotage des Conférences B , Руководящий комитет Международной конференции B ) организовал встречи, связанные с B-методом. ^[23] Он организовал конференции ZB с группой пользователей Z и конференции ABZ, включая абстрактные конечные автоматы (ASM) , а также нотацию Z.

Книги

• Книга 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, Пиза , Италия , 18–22 июня 2012 г.
• ABZ 2014, Тулуза , Франция, 2–6 июня 2014 г.
• ABZ 2016, Линц , Австрия , 23–27 мая 2016 г.
• ABZ 2018, Саутгемптон , Великобритания, 2018 г.
• ABZ 2020, Ульм , Германия , 2021 г. (отложено из-за пандемии COVID-19 )
• ABZ 2021, Ульм, Германия, 2021 г.

Смотрите также

• Формальные методы
• Z-обозначение

Рекомендации

1. Канселл, Доминик и Доминик Мери. «Основы метода Б». Вычислительная техника и информатика 22, вып. 3–4 (2003): 221–256.
2. Батлер, Майкл, Филипп Кернер, Себастьян Крингс, Тьерри Лекомт, Майкл Леушель, Луис-Фернандо Мехиа и Лоран Вуазен. «Первые двадцать пять лет промышленного использования Б-метода». На Международной конференции по формальным методам для промышленных критических систем, стр. 189-209. Спрингер , Чам, 2020 г.
3. Жан-Раймон Абриаль (1988). «Инструмент B (Аннотация)» (PDF) . В Блумфилде, Робин Э.; Маршалл, Линн С.; Джонс, Роджер Б. (ред.). ВДМ – Путь вперед, Учеб. 2-й симпозиум VDM-Европа . Конспекты лекций по информатике . Том. 328. Спрингер. стр. 86–87. дои : 10.1007/3-540-50214-9_8. ISBN 978-3-540-50214-2.
4. Абриал-младший, Мэтью К.О. Ли, Д.С. Нейлсон, П.Н. Шарбах и Иб Холм Соренсен. «Б-метод». На Международном симпозиуме VDM Europe, стр. 398-405. Шпрингер, Берлин, Гейдельберг, 1991.
5. Герхарт, Сьюзен, Д. Крейген и Тед Ралстон. «Пример: система сигнализации парижского метро». Программное обеспечение IEEE 11, вып. 1 (1994): 32–28.
6. Бем, Патрик, Поль Бенуа, Ален Февр и Жан-Марк Мейнадье. «МЕТЕОР: успешное применение Б в большом проекте». На Международном симпозиуме по формальным методам, стр. 369–387. Шпрингер, Берлин, Гейдельберг, 1999.
7. Леконт, Тьерри. «Применение формального метода в промышленности: 15-летняя траектория». На Международном семинаре по формальным методам для промышленных критических систем, стр. 26-34. Шпрингер, Берлин, Гейдельберг, 2009 г.
8. «Событие-B и платформа Родена». Event-B.org .
9. Батлер, Майкл. «Структуры декомпозиции для События-Б». На Международной конференции по интегрированным формальным методам, стр. 20–38. Шпрингер, Берлин, Гейдельберг, 2009 г.
10. Абриаль, Жан-Раймон. Моделирование в Event-B: системная и программная инженерия. Издательство Кембриджского университета , 2010.
11. Абриал, Жан-Раймонд, Майкл Батлер, Стефан Халлерстеде, Тай Сон Хоанг, Фархад Мехта и Лоран Вуазен. «Rodin: открытый набор инструментов для моделирования и рассуждений в Event-B». Международный журнал по программным инструментам для трансфера технологий 12, вып. 6 (2010): 447-466.
12. Хоанг, Тай Сон, Андреас Фюрст и Жан-Раймон Абриал. «Шаблоны Event-B и их инструментальная поддержка». Программное обеспечение и моделирование систем 12, вып. 2 (2013): 229–244.
13. "B-Инструментарий". [B-Core (UK) Limited] . 2004. Архивировано из оригинала 12 октября 2004 года . Проверено 22 февраля 2012 г.
14. Хотон, Ховард и Кевин Лано. Спецификация в B: введение в использование инструментария B. Всемирный научный, 1996.
15. Абриаль, Жан-Раймон. «Инструмент Б». На Международном симпозиуме VDM Europe, стр. 86-87. Шпрингер, Берлин, Гейдельберг, 1988.
16. Боуэн, Джонатан (июль 2022 г.). «Иб Холм Соренсен: десять лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 41–49 . Проверено 3 августа 2022 г.
17. Требования к B-Toolkit, заархивировано 12 октября 2004 г. на Wayback Machine.
18. Крайтон, Эдвард. «Исходный код B-Toolkit». Гитхаб .
19. "АтельеB.eu".
20. Ментре, Давид, Клод Марше, Жан-Кристоф Филлиатр и Масаси Аска. «Выполнение обязательств по доказательству от Ателье Б с использованием нескольких автоматических проверочных устройств». На Международной конференции по абстрактным государственным машинам, сплавам, B, VDM и Z, стр. 238-251. Шпрингер, Берлин, Гейдельберг, 2012 г.
21. Абриал, младший. «Процесс разработки системы с использованием Event-B и платформы Rodin». На Международной конференции по формальным инженерным методам, стр. 1-3. Шпрингер, Берлин, Гейдельберг, 2007 г.
22. Алджер, Аммар, Филипп Девьен, Софи Тайсон, JL. Буланже и Жорж Мариано. «BHDL: Схемотехника в B». На Третьей международной конференции по применению параллелизма в проектировании систем, 2003. Труды, стр. 241-242. ИИЭР, 2003.
23. "Ассоциация пилотажа конференций B" . librairiecosmopolite.com . Проверено 27 июля 2022 г.

Внешние ссылки

• B Method.com - работы и предметы, касающиеся метода B, формального метода с доказательством.
• Atelier B.eu. Архивировано 21 февраля 2008 г. в Wayback Machine : Atelier B — это мастерская системного проектирования, которая позволяет разрабатывать программное обеспечение, гарантированно безупречное.
• Зона Б Гренобль