B-метод

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

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

Обзор

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

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

Событие-Б

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

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

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

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

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

Уточнение

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

Выполнение

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

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

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

B -Toolkit ^{[13] [14]} — это набор программных инструментов, разработанных для поддержки использования B-Tool, ^[15] — это математический интерпретатор на основе теории множеств, предназначенный для поддержки B-Method. Разработка изначально велась Ибом Хольмом Сёренсеном и другими в 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 , а также для сертификации Common Criteria и разработки системных моделей компаниями 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-Book: Назначение программ значениям , Жан-Раймон Абриаль , Cambridge University Press , 1996. ISBN  0-521-49619-5 .
• B-метод: введение , Стив Шнайдер, Palgrave Macmillan , серия «Краеугольные камни вычислительной техники», 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 , Кевин Лано , 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-Method и/или Event-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 г.
• Б, от исследований к преподаванию, Нант, Франция, 16 июня 2008 г.
• Б, от исследований к преподаванию, Нант, Франция, 8 июня 2009 г.
• Б, от исследований к преподаванию, Нант, Франция, 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. Канселл, Доминик и Доминик Мери. «Основы метода B». Вычислительная техника и информатика 22, № 3-4 (2003): 221-256.
2. Батлер, Майкл, Филипп Кёрнер, Себастьян Крингс, Тьерри Леконт, Майкл Лёшел, Луис-Фернандо Мехия и Лоран Вуазен. «Первые двадцать пять лет промышленного использования B-метода». В Международной конференции по формальным методам для промышленных критических систем, стр. 189-209. Springer , Cham, 2020.
3. Жан-Раймонд Абриаль (1988). "Инструмент B (Аннотация)" (PDF) . В Bloomfield, Робин Э.; Маршалл, Линн С.; Джонс, Роджер Б. (ред.). VDM – Путь вперед, Proc. 2nd VDM-Europe Symposium . Lecture Notes in Computer Science . Vol. 328. Springer. pp. 86–87. doi :10.1007/3-540-50214-9_8. ISBN 978-3-540-50214-2.
4. Абриал, Дж. Р., Мэтью КО Ли, Д. С. Нильсон, П. Н. Шарбах и Иб Хольм Сёренсен. «B-метод». На Международном симпозиуме VDM Europe, стр. 398-405. Springer, Берлин, Гейдельберг, 1991.
5. Герхарт, Сьюзен, Д. Крейген и Тед Ралстон. «Исследование случая: система сигнализации парижского метро». IEEE Software 11, № 1 (1994): 32-28.
6. Бем, Патрик, Поль Бенуа, Ален Февр и Жан-Марк Мейнадье. "METEOR: успешное применение B в большом проекте". В Международном симпозиуме по формальным методам, стр. 369-387. Springer, Берлин, Гейдельберг, 1999.
7. Леконт, Тьерри. «Применение формального метода в промышленности: 15-летняя траектория». В Международном семинаре по формальным методам для критических промышленных систем, стр. 26-34. Springer, Берлин, Гейдельберг, 2009.
8. "Event-B и платформа Родена". Event-B.org .
9. Батлер, Майкл. "Структуры декомпозиции для события-B". В Международной конференции по интегрированным формальным методам, стр. 20-38. Springer, Берлин, Гейдельберг, 2009.
10. Абриаль, Жан-Раймонд. Моделирование в Event-B: системная и программная инженерия. Cambridge University Press , 2010.
11. Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta и Laurent Voisin. "Rodin: открытый набор инструментов для моделирования и рассуждений в Event-B". Международный журнал по программным инструментам для передачи технологий 12, № 6 (2010): 447-466.
12. Хоанг, Тай Сон, Андреас Фюрст и Жан-Раймонд Абриаль. «Шаблоны событий B и их инструментальная поддержка». Программное обеспечение и системное моделирование 12, № 2 (2013): 229-244.
13. "The B-Toolkit". [B-Core (UK) Limited] . 2004. Архивировано из оригинала 12 октября 2004 года . Получено 22 февраля 2012 года .
14. Хоутон, Ховард и Кевин Лано. Спецификация на языке B: Введение с использованием инструментария B. World Scientific, 1996.
15. Абриаль, Жан-Раймонд. «Инструмент B». На Международном симпозиуме VDM Europe, стр. 86-87. Springer, Берлин, Гейдельберг, 1988.
16. Боуэн, Джонатан (июль 2022 г.). «Ib Holm Sørensen: Ten Years After» (PDF) . FACS FACTS . № 2022–2. BCS-FACS . стр. 41–49 . Получено 3 августа 2022 г. .
17. Требования к B-Toolkit Архивировано 12 октября 2004 г. на Wayback Machine
18. Крайтон, Эдвард. «Исходный код B-Toolkit». GitHub .
19. "AtelierB.eu".
20. Ментре, Дэвид, Клод Марше, Жан-Кристоф Филлиатр и Масаси Асука. «Выполнение обязательств по доказательству из Atelier B с использованием нескольких автоматизированных доказывающих устройств». В Международной конференции по абстрактным конечным машинам, Alloy, B, VDM и Z, стр. 238-251. Springer, Берлин, Гейдельберг, 2012.
21. Абриал, Дж. Р. «Процесс разработки системы с Event-B и платформой Родена». В Международной конференции по формальным методам инжиниринга, стр. 1-3. Springer, Берлин, Гейдельберг, 2007.
22. Альджер, Аммар, Филипп Девьен, Софи Тисон, Ж. Л. Буланже и Жорж Мариано. «BHDL: проектирование схем на языке B». В Третьей международной конференции по применению параллелизма в проектировании систем, 2003. Труды., стр. 241-242. IEEE, 2003.
23. "Ассоциация пилотажа конференций B" . librairiecosmopolite.com . Проверено 27 июля 2022 г.

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

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