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

Этот механизм предусматривал следующие три основных действия. Прежде всего, информация о возникновении нештатной ситуации должна быть передана по шине на бортовой компьютер OBC; параллельно она вместе со всем контекстом записывалась в перепрограммируемую память EEPROM (которую во время расследования удалось восстановить и прочесть ее содержимое), и наконец, работа процессора IRS должна была аварийно завершиться. Последнее действие и оказалось фатальным именно оно, случившееся в ситуации, которая на самом деле была нормальной (несмотря на сгенерированное из-за незащищенного переполнения программное исключение), и привело к катастрофе.

Осмысление

Произошедшая с Ariane 5 катастрофа имела исключительно большой резонанс и по причине беспрецедентных материальных потерь, и вследствие очень оперативного расследования, характеризовавшегося к тому же открытостью результатов (впервые такая практика публичности была опробована при расследовании причин аварии космического корабля Challenger 1986 г.). Сразу стало очевидным, что данному событию суждено войти в историю не только космонавтики, но и программной инженерии. Поэтому неудивительно, что авария послужила поводом для оживленной дискуссии, в которой приняли участие многие известные специалисты.

Ж.-М. Жезекель (J.-M. Jezequel) и Б. Мейер (B.Meyer)[3] пришли к совершенно однозначному выводу: допущенная (и так и не выявленная) программная ошибка носит, по их мнению, чисто технический характер и коренится в некорректной практике повторного использования ПО. Более точная формулировка: роковую роль сыграло отсутствие точной спецификации повторно-используемого модуля.

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

В качестве панацеи в такого рода ситуациях авторы предложили задействовать принцип «Контрактного Проектирования» (что и неудивительно, ибо его разработчиком как раз и является Мейер[4]). Именно «контракт» в духе языка Eiffel, явным образом (с помощью пред- и пост-условий) устанавливающий для любого программного компонента ограничения на входные и выходные параметры, и мог бы предотратить катастрофическое развитие событий. Был приведен и набросок такого контракта:

^{convert (horizontal_bias: INTEGER): INTEGER is}

     ^require

          ^{horizontal_bias <= Maximum_bias}

               ^do

               ^…

          ^ensure

     ^…

^end

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

Однако, самым важным достоинством использования контрактных механизмов является, по мнению авторов, явное присутствие легко понимаемых и при необходимости верифицируемых ограничений как в документации, так и в коде.

При работе над сложными проектами типа Ariane именно контракты могли бы выступать в качестве опорных ориентиров для групп качества «QA Team», чья задача выполнять систематический мониторинг ПО на предмет соответствия требованиям. Авторы с сожалением заключают, что контрактные механизмы никак не получат должного распространения в современной практике. Более того, положение только усугубляется: например, в Java даже исчезла присутствовавшая в языке Cи скромная по возможностям инструкция «assert». В составной части CORBA языке IDL (Interface Definition Language), предназначенном обеспечить полномасштабное повторное использование компонентов в распределенной среде, отсутствует какой-либо механизм спецификации семантики. То же относится и к ActiveX. Авторы заключают: без полной и точной спецификации, основанной на пред- и пост-условиях и инвариантах, «повторное использование программных компонентов совершенное безрассудство».

Эта точка зрения вызвала многочисленные отклики. Хотя полезность использования контрактных механизмов никто не оспаривал, все же взгляд авторов многим показался упрощенным. Наиболее обстоятельный критический разбор их статьи выполнил сотрудник Locheed Martin Tactical AirCraft Systems, известный специалист в области разработки ответственных систем Кен Гарлингтон (Ken Garlington).[5] Он начал с того, что указал на ошибку в приведенном наброске контракта, где предполагается, что BH преобразуется не из вещественного (как то было в реальности) числа, а из целого.