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

Тогда в Б или не в Б? Давайте погрузимся в Б-метод вместе.

Что это может быть?

Б-метод — это не получение нектара из цветов для изготовления меда. Это довольно:

  1. формальный метод; это означает, что он основан на математическом формализме.
  2. с доказательством; доказательство гарантирует, что модель непротиворечива во всех возможных случаях использования.
  3. используется для моделирования системы или разработки программного обеспечения.

Хотя он не очень известен среди разработчиков программного обеспечения, B-метод используется во многих крупных промышленных проектах, вот некоторые из них:

KVB: Alstom —автоматическая защита поездов для французской железнодорожной компании (SNCF), установленная на 6000 поездов с 1993 года, 60 000 линий B; 10 000 доказательств; 22 000 строк Ады

SAET METEOR: Siemens Transportation Systems. —Автоматическое управление поездом, новая линия 14 метро без машинистов в Париже (RATP), 1998 г. 3 критически важные для безопасности программные части: бортовая, секция, линия 107 000 строк B; 29 000 доказательств; 87 000 строк языка Ада

EADS —Модель планирования задач программного обеспечения, управляющего разделением ступеней ракеты Ariane

Я надеюсь, что теперь B-метод привлек ваше внимание, давайте посмотрим больше.

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

Следует уточнить некоторые конкретные термины:

Абстрактная модель

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

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

Конкретная модель

Мы должны доказать, что конкретная модель соответствует своей спецификации (абстрактной модели), поскольку она является своего рода специализацией более абстрактной модели.

Существует также то, что называется уточнением, которое заключается в добавлении дополнительных деталей к модели, чтобы сделать ее более конкретной. В B-программном обеспечении это соответствует реализации (последней реализацией является сама программа) модели. (спецификация абстрактная или уточненная).​​

Вывод

B-software имеет множество преимуществ:

  • НЕТ классической ошибки программирования в коде (переполнение, деление на 0, индекс вне диапазона, бесконечный цикл, псевдонимы)
  • Модульные тесты больше не используются
  • Раннее обнаружение ошибок
  • Такие фреймворки, как AtelierB или Rodin, упрощают создание корректного кода POO на различных языках (C++, Ada, C, …).

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