Мифы о безопасном ПО - уроки знаменитых катастроф

Необходимость модернизации ПО диктовалась периодическим обновлением аппаратной базы, добавлением функциональности, а также происходило по причине необходимости исправления выявленных дефектов. По оценке независимых экспертов, эти модификации поначалу не сопровождались должными процедурами по поддержке безопасности, однако, случившаяся в 1986 г. авария с кораблем Challenger, которая хотя и произошла по причинам, не связанным с ПО, послужила толчком к пересмотру всей политики NASA в области безопасности, затронув и область ПО. 
Наконец, вряд ли справедливо мнение, что все более входящий в практику принцип повторного использования ПО дает повышенные гарантии безопасности. 
Мысль о том, что использование имеющего длительную историю и уже зарекомендовавшего себя с положительной стороны модуля, равно как и "коробочного" продукта, дает гарантии отсутствия в нем ошибок, весьма естественна с точки зрения "здравого смысла" и способна притупить бдительность. а самом деле повторное использование программных модулей может и понизить безопасность по той простой причине, что данные модули изначально разрабатывались и отлаживались для использования в ином контексте, а спецификация обычно не дает исчерпывающего отчета о всех видах возможного поведения модуля (произошедшая с Ariane 5 авария имеет основной причиной именно повторное использование модуля с некорректной для изменившегося контекста спецификацией). 
В случае с Therac-25 большой вклад в произошедшие инциденты внесли модули, изначально разработанные для предыдущей версии системы (Therac-20) во всяком случае, было точно установлено, что именно ошибки в этих повторно-используемых модулях вызвали по крайней мере два смертных случая. 
Причем, эти ошибки (как уже было установлено задним числом) проявлялись и при работе Therac-20, но та система была устроена так, что массивного переоблучения не происходило, а потому и процесс коррекции ошибок не запускался. 
Можно привести еще несколько любопытных иллюстраций к проблемам, связанным с повторным использованием. Так, попытка внедрить в Англии программную систему управления воздушным движением, которая до того несколько лет успешно эксплуатировалась в США, оказалась сопряжена с большими трудностями ряд модулей весьма оригинальным образом обращались с информацией о географической долготе: карта Англия уподоблялась листу бумаги, согнутому и сложенному вдоль Гринвичского меридиана, и получалось, что симметрично расположенные относительно этого нулевого меридиана населенные пункты накладывались друг на друга. В Америке, через которую нулевой меридиан не проходит, эти проблемы никак не проявлялись. Аналогично, успешно функционировавшее авиационное ПО, изначально написанное с неявным прицелом на эксплуатацию в северном полушарии, создавало проблемы, когда его стали использовать при полетах по другую сторону экватора. аконец, ПО, написанное для американских истребителей F-16, явилось причиной нескольких инцидентов, будучи использованным израильской авиацией при полетах над Мертвым морем, которое, как известно, находится ниже уровня моря. Это лишний раз подтверждает мысль, что безопасность ПО нельзя оценивать в отрыве от среды, в контексте которой эксплуатируется вся система. 
О "корректном" ПО 
Заветная мечта (не столько программистов, сколько потребителей), чтобы в ПО не было ошибок, увы, никак не исполняется. И иллюзий на этот счет уже не осталось. Соответственно, утверждение, что тестирование ПО и/или "доказательство" его корректности позволяют выявить и исправить все ошибки, можно признать тем мифом, в который мало кто верит. 
Причина очевидна. Прежде всего, исчерпывающее тестирование сложных программных систем невозможно в принципе: реально проверить только небольшую часть из всего пространства возможных состояний программы. В результате, тестирование может продемонстрировать наличие ошибок, но не может дать гарантию, что их нет. Как ядовито замечают Жезекель и Мейер [2], собственно, сам запуск Ariane 5 и явился весьма качественно выполненным тестом; правда, не каждый согласится платить полмиллиарда долларов за обнаружение ошибки переполнения. 
Что же касается использования математических методов для верификации ПО в плане его соответствия спецификации, то оно (несмотря на оптимизм, особенно явный в 70-х г.) пока не вошло в практику в сколько-нибудь значительном масштабе, хотя и сейчас некоторые влиятельные специалисты продолжают утверждать, что это непременно случится в будущем. Вопрос, реалистично ли ожидать, что для систем масштаба 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 тысяч лемм. асколько этот подход (и аналогичные ему) будет востребован практикой, покажет будущее.