Мифы о безопасном ПО - уроки знаменитых катастроф   ::   Аджиев Валерий

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

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

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

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

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