Есть так же метод Б (https://en.wikipedia.org/wiki/B-Method) с практическим применением например для автономной ветки метро или космического корабля Ариан-5.

Желающие могут самостоятельно попробовать — «Atelier B is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software)». На выходе автоматически генерируется код на С или Ада.

Ссылки:
www.atelierb.eu/en
www.atelierb.eu/wp-content/uploads/sites/3/dbprotect/formations/slides/formation-atelier-b-formation-niveau-1-en.pdf

Интервью Jean-Raymond Abrial (создатель метода Б) для журнала 01net о формальных методах в 2002г (извиняюсь за корявый перевод).

www.01net.com/actualites/jean-raymond-abrial-consultant-le-zero-defaut-nexiste-pas-mais-on-peut-tout-de-meme-sen-approcher-173964.html

Формальные методы повышают надёжность программного обеспечения, но их использование не распространено. Как вы это объясните?

Возможно некоторые производители софта не заинтересованны в том чтобы он корректно работал. Что действительно происходит с широко используемыми программными продуктами. Ко всему прочему ещё потому, что много юзеров любят возится (с софтом) и если что-то хорошо работает, это для них не интересно. Таким образом дисфункционирование программного обеспечения может быть желаемым и рассматриваться как плюс. Но здесь я привожу только положительные стороны. Я не имею в виду профессионалов, которые делают это специально, чтобы затем клиент платил за поддержку. Использование формальных методов с подобными идеями не представляет интереса, так как программа будет работать корректно. Тогда как использование этих методов для гарантии того, что автоматический беспилотный поезд или спутник выполнят правильно свои миссии, имеет смысл.

Формальные методы подразумевают затраты большего времени на спецификацию, чем на тесты. Не ставит ли это под сомнение обычный цикл разработки?

В других инженерных дисциплинах, таких как авиаконструирование или гражданское строительство существуют аналоги формальных методов — это понятие конструкторского бюро. Сначала рисуют модель будущего объекта, который затем осмысляют в соответствии с теориями. Идея долгого процесса от осмысления до реализации есть часть современной инженерии. Использование формальных методов это конструкторское бюро программного обеспечения: рисунок софта это формальный объект который мы не можем запустить, но над которым мы можем размышлять, моделировать. Большинство программистов считают, что достаточно запустить программу и провести тесты для того, чтобы убедится в правильном функционировании. Как если бы для создания самолета, вы производите что-то похожее на утюг с крыльями и который затем тестируете. Этот способ практиковался в истории технологий, но это примитивный подход. С момента как технология набирает значимости, мы начинаем размышлять над чертежами и моделями.

В чем сложность использования формальных методов?

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

В каких случаях формальные методы наиболее применимы?

Их достаточно много. Например концепция распределенных систем: проблема в том, что в них не существует «главного». В протоколе маршрутизации узел сети не предпринимает решений за другие узлы. Информация меняется и на каждом узле заново определяется дальнейший маршрут, в зависимости от особенностей локальной сети. Таким образом, очень трудно проводить тесты в подобных условиях, так как эти условия исполнения никогда не повторяются. Формальные методы, отчасти, используются для разработки протоколов передачи, маршрутизации и криптографии. Эти методы все больше и больше применяются в задачах, которые неограниченны лишь разработкой софта. В частности, при изучении сложных систем. Необходимо реализовать объект, над которым будет производится дальнейшее размышление, строго соответствующее модели объекта.

В каких странах более всего используются формальные методы?

Европа немного впереди планеты всей. В частности Франция, Англия и Германия. Что же касается американцев, то и них много денег и хорошие методы работы. Люди, участвующие в проекте, очень ответственны. Это компенсирует часть проблемы. В профессиональном отношении, они придают огромное значение качеству специалистов. Кстати, в больших компаниях можно часто встретить высокопоставленных работников, которые сами являются специалистами (в тексте техниками). Технические знания высоко ценятся, это позволяет создавать качественные системы.

Являются ли формальные методы панацеей?

Сто процентное качество не существует, всегда что-то может произойти. Если мы установим компьютер в туннеле с множеством электрических помех, значение бита/байта может спонтанно поменяться. Те, кто считают что могут достигнуть отсутствие дефектов не являются настоящими инженерами. Но к этой цели мы можем приблизится. Инженер всегда размышляет с учётом вероятности и в сознании этого он учитывает любой риск, каким бы минимальным он не был.

Jean-Raymond Abrial, независимый консультант и «изобретатель» формального метода B.