B-метод - B-Method

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

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

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

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

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

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

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

Уточнение

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

Выполнение

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

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

B-Toolkit

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

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

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

Ателье Б

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

Он используется для разработки автоматов безопасности для различных метро, ​​установленных по всему миру. Alstom и Сименс, а также для сертификации Common Criteria и разработки моделей системы АТМЕЛ и STMicroelectronics.

Книги

  • B-Book: соотнесение программ со смыслами, Жан-Раймон Абриаль, Издательство Кембриджского университета, 1996. ISBN  0-521-49619-5.
  • B-метод: введение, Стив Шнайдер, Пэлгрейв Макмиллан, Серия Cornerstones of Computing, 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, Кевин Лано, Всемирная научная издательская компания, Imperial College Press, 1996. ISBN  1-86094-008-0.
  • Моделирование в Event-B: системная и программная инженерия, Жан-Раймон Абриаль, Издательство Кембриджского университета, 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 г.
  • Б. От исследований к преподаванию, Нант, Франция, 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)

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

  1. ^ Жан-Раймон Абриаль (1988). "Инструмент Б (Аннотация)" (PDF). В Робин Э. Блумфилд и Линн С. Маршалл и Роджер Б. Джонс (ред.). VDM - Путь вперед, Proc. 2-й симпозиум VDM-Europe. Конспект лекций по информатике. 328. Springer. С. 86–87. Дои: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. ^ "Би-Core (UK) Limited". Данные компании Rex. Получено 22 февраля, 2012.
  6. ^ Исходный код B-Toolkit
  7. ^ "AtelierB.eu".

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

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

Статья основана на материалах, взятых из Бесплатный онлайн-словарь по вычислительной технике до 1 ноября 2008 г. и зарегистрированы в соответствии с условиями «перелицензирования» GFDL, версия 1.3 или новее.