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

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

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

Причина очевидна. Прежде всего, исчерпывающее тестирование сложных программных систем невозможно в принципе: реально проверить только небольшую часть из всего пространства возможных состояний программы. В результате, тестирование может продемонстрировать наличие ошибок, но не может дать гарантию, что их нет. Как ядовито замечают Жезекель и Мейер [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 тысяч лемм. асколько этот подход (и аналогичные ему) будет востребован практикой, покажет будущее.

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

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

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

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