B-метод

B — загальний термін, яким називають B-Method (формальний метод розробки програмного забезпечення), процес такої розробки, мову запису специфікації, і інструменти що їх підтримують (B-Toolkit)

Історія

Метод розроблений Жаном-Реймондом Абріалем у Великій Британії та Франції.

Використовувався при створенні в Європі систем критичних щодо надійності (помилка в яких створює небезпеку для людей та інших ресурсів). Наприклад 14 лінія паризького метро

Недавно створили ще один метод, названий Event-B. Він розглядається як вдосконалення B (відомого також як класичний B). Event-B має простіший синтаксис, що полегшує його вивчення та використання. Інструменти, що його підтримують, називаються платформою Rodin.

B-Method

B-Method — це набір математичних технологій для специфікації, проектування та реалізації компонент програмного забезпечення. Системи моделюються як сукупності незалежних Абстрактних Машин, для яких на всіх стадіях розробки застосовується об'єктно-орієнтований підхід.

Абстрактна Машина описується з використанням Abstract Machine Notation (AMN). Стандартна нотація використовується на всіх рівнях опису, від специфікації до реалізації.

AMN — мова формальної специфікації, що базується на станах. Вона вийшла з тієї ж школи, що і VDM та Z. Абстрактна машина включає стан разом з операціями на тому стані. У специфікаціях та конструюванні Абстрактної Машини стани моделюються з використанням таких понять як множина, відношення, функція, послідовність та подібних. Оператори моделюються з використанням перед- та післяумов.

У реалізації абстрактної машини стан знову моделюється з використанням теоретико-множинної моделі, але цього разу ми вже маємо реалізацію цієї моделі. Ця операція описується з використанням псевдокоду, який є підмножиною AMN.

Математичний запис

Примітки

1. en:Paris Métro Line 14#The Meteor Project

Посилання

1. http://www.event-b.org/ [ 3 червня 2010 у Wayback Machine.]