Из Википедии, свободной энциклопедии
  (Перенаправлен из Event-B )
Перейти к навигации Перейти к поиску

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

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

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

Основные компоненты [ править ]

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

Абстрактная машина [ править ]

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

Уточнение [ править ]

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

Реализация [ править ]

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

Программное обеспечение [ править ]

B-Toolkit [ править ]

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

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

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

Ателье Б [ править ]

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

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

Книги [ править ]

  • Книга B: Назначение программ значениям , Жан-Раймон Абриаль , Cambridge University Press , 1996. ISBN  0-521-49619-5 .
  • B-метод: введение , Стив Шнайдер, Пэлгрейв Макмиллан , серия Cornerstones of Computing, 2001. ISBN 0-333-79284-X . 
  • Разработка программного обеспечения с Б. , Джон Вордсворт, Аддисон Уэсли Лонгман , 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 . 
  • Моделирование в событии-B: системная и программная инженерия , Жан-Раймон Абриаль , Cambridge University Press , 2010. ISBN 978-0-521-89556-9 . 

Конференции [ править ]

  • Конференция Z2B, Нант, Франция, окт. 10-12 1995
  • Первая конференция B, Нант, Франция, ноябрь. 25-27 1996 г.
  • Вторая конференция B, Монпелье, Франция, ap. 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 (Association de Pilotage des Conférences B)

Ссылки [ править ]

  1. ↑ Жан-Раймон Абриаль (1988). "Инструмент B (Аннотация)" (PDF) . В Робин Э. Блумфилд и Линн С. Маршалл и Роджер Б. Джонс (ред.). VDM - Путь вперед, Proc. 2-й симпозиум VDM-Europe . Конспект лекций по информатике . 328 . Springer. С. 86–87. DOI : 10.1007 / 3-540-50214-9_8 . ISBN  978-3-540-50214-2.
  2. ^ Event-B.org - Event-B и платформа Родена .
  3. ^ "B-Toolkit" . [B-Core (UK) Limited] . 2004. Архивировано из оригинального 12 октября 2004 года . Проверено 22 февраля 2012 года .
  4. ^ B-Toolkit Требования Архивировано 2004-10-12 в Wayback Machine
  5. ^ "B-Core (UK) Limited" . Компания Data Rex . Проверено 22 февраля 2012 года .
  6. ^ Исходный код B-Toolkit
  7. ^ "AtelierB.eu" .

Внешние ссылки [ править ]

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

Эта статья основана на материалах, взятых из Free On-line Dictionary of Computing до 1 ноября 2008 г. и включенных в соответствии с условиями «перелицензирования» GFDL версии 1.3 или новее.