"Валерий Аджиев "Мифы о безопасном ПО: уроки знаменитых катастроф" [V]" - читать интересную книгу автора

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

Формальные методы разработки это тема специального большого разговора.
Здесь же в качестве примера формального подхода, имеющего промышленные
перспективы, упомянем только "B-Method" [9], получивший недавно широкое
паблисити в связи с созданием ПО для автоматического управления движением
на одной из линий парижского метро. Разработчик метода Жан-Раймон Абриал
(J.-R.
Abrial), до того известный как создатель формального метода Z
(вошедшего в учебные программы всех уважающих себя университетов),
использовал идеи таких классиков, как Эдсгар Дийкстра (E.W.Dijkstra) и
Тони Хоар (C.A.R.Hoare).
Важно, что основанная на формализмах методология поддержана
практической инструментальной средой разработки Atelie B (которая, кстати,
не единственная).

Эта среда включает в себя инструменты для статической верификации
написанных на B-коде компонентов и для автоматического выполнения
доказательств, автоматические трансляторы из B-кода в Си и Ада,
повторно-используемые библиотеки B-компонентов, средства графического
представления проектов и генерации документации, гипертекстовый навигатор
и аниматор, позволяющий в интерактивном режиме моделировать исполнение
проекта из спецификации, и, наконец, средства по управлению проектом. При
разработке ПО для метро, включавшего около 100 тысяч строк B-кода (что
эквивалентно 87 тыс. строк на Ада) пришлось доказать около 28 тысяч лемм.
асколько этот подход (и аналогичные ему) будет востребован практикой,
покажет будущее.

И все же, такого рода верификация все равно не способна решить все
проблемы, в частности, потому, что требуется специфицирование "корректного
поведения" программной системы на формальном математическом языке, а это
может быть очень непросто. К тому же, источник многих потенциально опасных
ошибок может быть не связан непосредственно с вычислительными и
алгоритмическими аспектами. апример, в 1992 г. большой резонанс получил
произошедший в Англии случай, когда "пошел в разнос" компьютер на станции
скорой помощи: причина неожиданно проявившиеся трудности с синхронизацией
процессов в условиях большого количества поступивших заявок.


О "надежном" ПО

Теперь о менее очевидном мифе, который звучит так:
программно-аппаратные системы обеспечивают заведомо большую надежность по