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-Инструментарий

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

БХДЛ

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

АПЦБ

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 — это мастерская системного проектирования, которая позволяет разрабатывать программное обеспечение, гарантированно безупречное.
Зона Б Гренобль

[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 г.

[event-b-8] Jump up to: ^а ^б ^с «Событие-Б и платформа Родена» . Event-B.org .

[9] Батлер, Майкл. «Структуры декомпозиции для События-Б». На Международной конференции по интегрированным формальным методам, стр. 20–38. Шпрингер, Берлин, Гейдельберг, 2009 г.

[10] Абриаль, Жан-Раймон. Моделирование в Event-B: системная и программная инженерия. Издательство Кембриджского университета , 2010.

[rodin10-11] Jump up to: ^а ^б Абриал, Жан-Раймонд, Майкл Батлер, Стефан Халлерстеде, Тай Сон Хоанг, Фархад Мехта и Лоран Вуазен. «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.

[ihs22-16] Боуэн, Джонатан (июль 2022 г.). «Иб Холм Соренсен: десять лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 41–49 . Проверено 3 августа 2022 г.

[17] Требования к B-Toolkit , заархивировано 12 октября 2004 г. на Wayback Machine.

[18] Крайтон, Эдвард. «Исходный код B-Toolkit» . Гитхаб .

[19] «АтельеБ.еу» .

[20] Ментре, Давид, Клод Марше, Жан-Кристоф Филлиатр и Масаси Аска. «Выполнение обязательств по доказательству от Ателье Б с использованием нескольких автоматических проверочных устройств». На Международной конференции по абстрактным государственным машинам, сплавам, B, VDM и Z, стр. 238-251. Шпрингер, Берлин, Гейдельберг, 2012 г.

[21] Абриал, младший. «Процесс разработки системы с использованием Event-B и платформы Rodin». На Международной конференции по формальным инженерным методам, стр. 1-3. Шпрингер, Берлин, Гейдельберг, 2007 г.

[22] Алджер, Аммар, Филипп Девьен, Софи Тайсон, JL. Буланже и Жорж Мариано. «BHDL: Схемотехника в B». На Третьей международной конференции по применению параллелизма в проектировании систем, 2003. Труды, стр. 241-242. ИИЭР, 2003.

[23] «Ассоциация управления конференциями B» . книжный магазинcosmopolite.com . Проверено 27 июля 2022 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]