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

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

Можно привести еще несколько любопытных иллюстраций к проблемам,
связанным с повторным использованием. Так, попытка внедрить в Англии
программную систему управления воздушным движением, которая до того
несколько лет успешно эксплуатировалась в США, оказалась сопряжена с
большими трудностями ряд модулей весьма оригинальным образом обращались с
информацией о географической долготе: карта Англия уподоблялась листу
бумаги, согнутому и сложенному вдоль Гринвичского меридиана, и получалось,
что симметрично расположенные относительно этого нулевого меридиана
населенные пункты накладывались друг на друга. В Америке, через которую
нулевой меридиан не проходит, эти проблемы никак не проявлялись.
Аналогично, успешно функционировавшее авиационное ПО, изначально
написанное с неявным прицелом на эксплуатацию в северном полушарии,
создавало проблемы, когда его стали использовать при полетах по другую
сторону экватора. аконец, ПО, написанное для американских истребителей
F-16, явилось причиной нескольких инцидентов, будучи использованным
израильской авиацией при полетах над Мертвым морем, которое, как известно,
находится ниже уровня моря. Это лишний раз подтверждает мысль, что
безопасность ПО нельзя оценивать в отрыве от среды, в контексте которой
эксплуатируется вся система.


О "корректном" ПО

Заветная мечта (не столько программистов, сколько потребителей), чтобы
в ПО не было ошибок, увы, никак не исполняется. И иллюзий на этот счет уже
не осталось. Соответственно, утверждение, что тестирование ПО и/или
"доказательство" его корректности позволяют выявить и исправить все
ошибки, можно признать тем мифом, в который мало кто верит.

Причина очевидна. Прежде всего, исчерпывающее тестирование сложных
программных систем невозможно в принципе: реально проверить только
небольшую часть из всего пространства возможных состояний программы. В
результате, тестирование может продемонстрировать наличие ошибок, но не
может дать гарантию, что их нет. Как ядовито замечают Жезекель и Мейер
[2], собственно, сам запуск Ariane 5 и явился весьма качественно
выполненным тестом; правда, не каждый согласится платить полмиллиарда
долларов за обнаружение ошибки переполнения.

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