Программы и их модели

Усложнение программных комплексов для реальных систем вызывает рост требований к их надежности. Достаточно хотя бы вспомнить катастрофу ракеты «Ариан-5», взорвавшейся 4 июня 1996 г. в результате сбоя программного обеспечения — некорректное преобразование 64-разрядного числа в 16-разрядное, привело к исключительной ситуации и нарушению работы основного и дублирующего компьютеров, которые выдали, в результате, ошибочные данные о высоте полета. Среди мер, предотвращающих подобные происшествия, комиссия по расследованию инцидента отметила важную роль верификации программного обеспечения.

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

Написанная группой авторов во главе с Э.М. Кларком книга посвящена верификации программ на основе их модели. Отмечая во введении тенденцию к росту требований по надежности систем в целом, авторы аргументируют интерес к совершенствованию технологий проверки надежности ПО его усложнением и увеличением зависимости людей от правильности функционирования программ. Объемы таких проверок растут, соответственно, существует проблема их автоматизации. Чтобы определиться с методологией проверок ПО, авторы книги предлагают model checking, или проверку на модели ПО — «… автоматический метод верификации параллельных систем с конечным числом состояний». Раз речь в книге идет о моделях программ, то в ней приводится формальное описание моделей, которое и определяет методологию проведения проверок. Среди основных методов проверки правильности работы сложных программных комплексов традиционно используются имитационное моделирование, тестирование, дедуктивный анализ и проверка на модели.

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

Применение метода проверки программ на моделях авторы книги рассматривают в рамках этапов моделирования, спецификации и верификации. Для чего сначала проектируемый комплекс программ приводят к формальному виду удобному для инструментальных средств верификации моделей программ. Затем формулируют свойства, которыми должен обладать проектируемый комплекс. При этом для аппаратных средств и программного обеспечения используют логику, добиваясь полноты спецификации. Наконец, осуществляется этап спецификации, но лишь в идеальном случае он осуществляется полностью автоматически. Часто проведение проверок невозможно из-за так называемого комбинаторного взрыва — значительного роста объема проверок даже при небольшом усложнении модели комплекса программ.

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

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

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