B-метод

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

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

Впоследствии был разработан другой формальный метод, названный Event-B ^[2] . Событие-B считается эволюцией B (также известного как классическое B). Это более простая нотация, которую легче ^{изучить и использовать} . Он поставляется с поддержкой инструментов в виде инструмента Rodin .

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

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

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

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

Уточнение

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

Выполнение

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

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

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

B - Toolkit ^[3] , разработанный Ib Holm Sørensen et al. , представляет собой набор инструментов программирования, предназначенных для поддержки использования B-Tool, математического интерпретатора, основанного на теории множеств, в целях формальной методологии разработки программного обеспечения, известной как B-метод.

Инструментарий использует пользовательский интерфейс X Window Motif ^[4] для управления графическим интерфейсом и работает в основном в операционных системах Linux , Mac OS X и Solaris . Он был разработан британской компанией B-Core (UK) Limited. ^[5]

Теперь доступен исходный код B-Toolkit. ^[6]

Ателье Б

^{Atelier B [7]} , разработанный ClearSy, представляет собой промышленный инструмент, который позволяет оперативно использовать метод B для разработки бездефектного проверенного программного обеспечения (формальное программное обеспечение). Доступны две версии: Community Edition доступна для всех без каких-либо ограничений, Maintenance Edition только для держателей контрактов на техническое обслуживание.

Он используется для разработки автоматов безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens , а также для сертификации Common Criteria и разработки моделей систем компаниями ATMEL и STMicroelectronics .

Книги

• Книга B: Назначение программ значениям , Жан-Раймонд Абриал , издательство Кембриджского университета , 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 Toolkit , Кевин Лано , World Scientific Publishing Company , Imperial College Press , 1996. ISBN 1-86094-008-0 . 
• Моделирование в Event-B: System and Software Engineering , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN 978-0-521-89556-9 . 

Конференции

• Конференция 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'05, Гилфорд, Великобритания, 2005 г.
• B'2007, Безансон, Франция, 2007 г.
• B, от исследований к обучению, Нант, Франция, 16 июня 2008 г.
• B, от исследований к преподаванию, Нант, Франция, 8 июня 2009 г.
• B, от исследований к обучению, Нант, Франция, 7 июня 2010 г.
• Конференция ABZ: ABZ 2008, Британское компьютерное общество, Лондон, Великобритания, 16–18 сентября 2008 г.
• Конференция ABZ: ABZ 2010, Оксфорд, Квебек, Канада, 23–25 февраля 2010 г.
• Конференция ABZ: ABZ 2012, Пиза, Италия, 18–22 июня 2012 г.
• Конференция ABZ: ABZ 2014, Тулуза, Франция, 2–6 июня 2014 г.
• Конференция ABZ: ABZ 2016, Линц, Австрия, 23–27 мая 2016 г.

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

• APCB (Ассоциация пилотажных конференций B)
• БДЛ

использованная литература

внешняя ссылка

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