Вельдер С.Э. и др. Верификация автоматных программ

Подождите немного. Документ загружается.

На практике для того, чтобы убедиться, что конечный результат

выполняет то, что предписано, применяются два метода: экспертный

анализ и тестирование. Исследования в области разработки программ

показывают, что 80% всех проектов используют экспертный анализ –

полностью ручную деятельность, в которой прототип или его часть

исследуется командой специалистов, которые не были вовлечены в

процесс разработки этой компоненты системы. Тестирование является

важным методом валидации для проверки корректности полученных

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

инструментальной поддержке уделяется мало внимания.

Валидация систем – это важный шаг в их разработке: в большинстве

проектов больше времени и усилий уходит на валидацию, чем на

разработку. Ошибки могут быть очень дорогими. Например, ошибка в

денверской системе управления багажом задержала открытие нового

аэропорта на девять месяцев (ущерб – 1,1 миллиона долларов за день).

Валидация систем как часть процесса разработки

Интервью со специалистами ряда компаний, занимающихся

разработкой программного обеспечения, в очередной раз показало,

что валидация систем должна интегрироваться в процесс разработки

на ранних этапах [1, 3, 4]. Это справедливо, в том числе, и с

экономической точки зрения, однако в настоящее время большую

часть ошибок находят в процессе тестирования, когда программные

модули уже скомпонованы и исследуется вся система.

Формальные методы

Для обеспечения качества сложных программных систем требуется

использовать современные методы и инструменты, которые

поддерживают процесс валидации. Применяемые в настоящее время

методы валидации являются узкоспециализированными и базируются

на спецификациях, сформулированных на естественном языке.

Поэтому в данной книге рассматриваются подходы к валидации,

базирующиеся на формальных методах. При использовании таких

методов проектирование систем должно быть определено в терминах

точных и недвусмысленных спецификаций, которые предоставляют

базу для систематического анализа. Перечислим основные подходы к

валидации:

 симуляция;

 тестирование;

 формальная верификация;

 проверка моделей (верификация на моделях).

В дальнейшем будут кратко рассмотрены три первых подхода, а

основной темой, как отмечалось выше, является проверка моделей.

Реактивные системы

В данной книге основное внимание уделяется валидации реактивных

систем. Реактивные системы [5] характеризуются непрерывным

взаимодействием с окружением. Они принимают значения входов из

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

них. Типичными примерами систем этого класса являются

операционные системы, системы управления самолетами,

автомобилями и технологическими процессами, коммуникационные

протоколы и т. д. Например, система управления химическим

процессом регулярно принимает управляющие сигналы, такие как

температура и давление, в различных точках процесса. На основании

этой информации программа может принять решение включить

нагревательный элемент, выключить насос и т. д. Если возникла

опасная ситуация, например, давление в резервуаре выходит за

определенные пределы, управляющая программа должна выполнить

определенные действия. Обычно подобные реактивные системы

достаточно сложны.

Как отмечалось выше, корректность реактивных систем имеет

решающее значение. Для построения корректно работающей

реактивной системы требуется четкая методология, в которой

выделяются следующие фазы.

 На основе исчерпывающего анализа требований должна быть

сформирована их спецификация.

 Концептуальное проектирование позволяет получить абстрактную

спецификацию проекта. Эта спецификация может быть проверена

на непротиворечивость и ее соответствие требованиям. Данный

процесс валидации может быть поддержан формальной

верификацией, симуляцией и проверкой моделей – такими

процессами, в которых модель абстрактной спецификации проекта

(например, система конечных автоматов) может быть

исчерпывающим образом проверена.

 Когда заслуживающая доверия спецификация получена, переходят

к построению системы, которая реализует абстрактную

спецификацию. При этом тестирование является полезным

методом проверки реализации на соответствие оригинальным

требованиям.

1.2. Симуляция

Симуляция базируется на модели, которая описывает возможное

поведение системы. Эта модель в определенном смысле исполнима,

при этом программный инструмент (называемый симулятором) может

определить поведение системы по отношению к некоторым

сценариям. Таким способом пользователь получает определенное

понимание того, как система реагирует на стимулы. Сценарии могут

быть предоставлены пользователем или инструментом, таким как,

например, генератор, который строит случайные сценарии.

Симуляция, в основном полезна для быстрой, первоначальной оценки

качества проекта. Она в меньшей степени подходит для поиска тонких

ошибок, так как симулировать все возможные сценарии непрактично

(и часто невозможно).

1.3. Тестирование

Как отмечалось выше, широко используемым традиционным путем

валидации корректности проекта является тестирование [6]. В

тестировании система используется в том виде, в каком она

реализована (программа, устройство или их комбинация). На ее вход

подаются определенные значения входных данных, называемых

тестами, и исследуется реакция системы. После этого проверяется,

действительно ли реакция системы соответствует требуемому выходу.

Принципы тестирования почти такие же, как и у симуляции. Их

важное различие состоит в том, что тестирование проводится на

действующей реализации системы, а симуляция – на модели системы.

Тестирование – это метод валидации, широко используемый на

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

эвристических методов. Так как тестирование базируется на

рассмотрении только небольшого подмножества возможных примеров

поведения системы, оно никогда не может быть полным. Э. Дейкстра

отметил, что тестирование может показать только наличие ошибок, но

не их отсутствие.

Тестирование, однако, может дополнять формальную верификацию и

проверку моделей, которые выполняются на математической модели

системы, а не на реальной системе. Так как тестирование применяется

к реализации, оно полезно, главным образом, в следующих случаях:

 когда корректную модель системы сложно построить;

 когда части системы не могут быть формально промоделированы

(например, физические устройства);

 когда модель проприетарна.

Обычно, тестирование – доминирующий метод валидации систем. Он

состоит в применении к реализации ряда тестов, которые обычно

получают эвристически. В последнее время, однако, возрастает

интерес к применению формальных методов в тестировании.

Например, в области коммуникационных протоколов этот тип

исследований привел к проекту международного стандарта

«Формальные методы в тестировании пригодности» [7]. В нем

процесс тестирования разделен на несколько фаз:

1. Генерация тестов. Абстрактные описания тестов систематически

генерируются на основе точного и недвусмысленного задания

требуемых свойств в спецификации.

2. Выбор тестов. Выбирается множество образцов абстрактных

описаний тестов.

3. Реализация тестов. Абстрактные описания тестов

трансформируются в исполнимые тесты.

4. Исполнение тестов. Исполнимые тесты применяются к

тестируемой реализации путем выполнения их на тестирующей

системе. Рассматриваются и протоколируются результаты

исполнения.

5. Тестовый анализ. Запротоколированные результаты

анализируются с целью определения, удовлетворяют ли они

ожидаемым результатам.

Различные фазы тестирования могут пересекаться и на практике часто

пересекаются, особенно последние.

Тестирование – это метод, который может быть применен как к

прототипам, в форме систематической симуляции, так и к конечным

продуктам. Известны два базовых подхода: тестирование белого

ящика, когда внутренняя структура реализации может наблюдаться и

иногда частично управляться (стимулироваться), и тестирование

черного ящика [8]. Во втором случае может быть проверена только

коммуникация между тестируемой системой и окружением, а

внутренняя структура «ящика» полностью скрыта от тестера. В

практических обстоятельствах тестирование находится где-то между

этими двумя крайними случаями и иногда называется тестированием

серого ящика.

Перечислим основные виды тестов.

1. Модульные тесты (Unit tests). Тест пишется на класс, отдельный

метод этого класса и т. д. Обычно проверяется один сценарий

использования класса, метода или иного модуля.

2. Функциональные тесты. Тестируется не элемент кода, а

функциональность. Такие тесты позволяют выявлять структурные

ошибки.

3. Приемочные тесты. Проверяется, что программа делает именно то,

что хотел заказчик.

4. Стресс-тест. Тестируется работоспособность программы под

сильной нагрузкой.

5. Тест на дурака (monkey test). Программе подаются случайные

входные данные, и проверяются ее работоспособность на таких

данных и отказоустойчивость. Также проверяется наличие

уязвимостей. Такие тесты особенно важны для серверных

приложений.

6. Параллельные тесты. Проверяется, что новая версия работает так

же, как старая.

7. Регрессионные тесты. Пишутся после сообщения об ошибке. Тест

повторяет сценарий, при котором произошла ошибка.

Разработка через тестирование (Test-driven development)

Одной из технологий разработки программного обеспечения является

разработка через тестирование (test-driven development – TDD) [9].

Отметим, что TDD не является технологией тестирования. Этот

процесс состоит из коротких итераций разработки программы, каждая

из которых состоит из следующих этапов:

1. Написание теста.

2. Компиляция теста. Тест не должен компилироваться. Если тест

компилируется, то это означает, что создана сущность, которая уже

присутствует.

3. Устранение ошибки компиляции.

4. Запуск теста. Тест не должен проходить.

5. Написание кода. Пишется максимально простой код, какой только

возможен.

6. Прогон теста. На этот раз тест должен быть пройден.

7. Рефакторинг (если требуется).

Второй и третий этапы выполняются только при создании новых

модулей или классов.

Когда программа использует оборудование, доступ к которому

затруднен, применяются мок-объекты или моки [9] (mocks). Моки –

это автоматически сгенерированные заглушки. Также моки могут

использоваться для программирования сверху вниз [10]. Для создания

мок-объектов существуют специальные фреймворки (RhinoMock,

NMock, JMock и др.).

Свойства разработки через тестирование:

 подход заставляет разрабатывать программу с точки зрения

пользователя;

 он заставляет писать классы, независимые друг от друга;

 тесты являются также и документацией к коду;

 требуется много времени для того, чтобы освоить этот подход на

практике.

1.4. Формальная верификация

Дополняющим методом к симуляции и тестированию является

строгое доказательство того, что система работает корректно. Такая

математическая демонстрация корректности системы называется

формальной верификацией [11]. Базовая идея состоит в том, чтобы

построить формальную (математическую) модель исследуемой

системы, которая отражает (специфицирует) возможное поведение

системы. При этом требования корректности записываются в виде

формальной спецификации требований, которая отражает желаемое

поведение системы. На базе этих двух спецификаций можно

формальным доказательством проверить, действительно ли

возможное поведение согласуется с желаемым. Поскольку имеет

место верификация в математической форме, представление о

согласованности может быть точным, и верификация состоит в

доказательстве корректности по отношению к этому формальному

представлению.

Для формальной верификации требуются:

 Модель системы, обычно содержащая множество состояний,

которые хранят информацию о значениях переменных,

программных счетчиках и т. п., и отношение переходов, которое

описывает, как система переходит из одного состояния в другое.

 Метод спецификации для выражения требований в формальном

виде.

 Множество правил доказательства, позволяющих определить,

удовлетворяет ли модель сформулированным требованиям.

Для того чтобы более конкретно понять, что имеется в виду,

рассмотрим способ, с помощью которого могут быть формально

верифицированы последовательные программы.

Верификация последовательных алгоритмов

Этот подход может быть использован для доказательства

корректности последовательных алгоритмов [1, 12], таких как быстрая

сортировка или вычисление наибольшего общего делителя двух

целых чисел. Кратко опишем, как он работает. Он начинается с

формализации желаемого поведения с использованием пред- и

постусловий на основе формул логики предикатов. Синтаксис этих

формул можно определить, например, следующим образом:

φ ::= p | φ | (φ  φ).

Здесь p – базовое предложение (например, «x равно 2»), символ «» –

отрицание, а символ «» – дизъюнкция. Другие логические связки

могут быть определены следующим образом: φ  ψ = (φ  ψ),

true = φ  φ, false = true и φ  ψ = φ  ψ. Для простоты опустим

кванторы существования и всеобщности.

Предусловие описывает множество исследуемых стартовых состояний

(допустимых значений входов), а постусловие – множество желаемых

финальных состояний (требуемых значений выходов). Когда пред- и

постусловия формализованы, алгоритм кодируется в некотором

абстрактном псевдокоде, и по шагам доказывается, что он

удовлетворяет спецификации.

Для построения доказательств используется формальная система –

множество правил вывода. Эти правила обычно соответствуют

построению программы (алгоритма). Они записываются следующим

образом:

{φ} S {ψ}.

Здесь φ – предусловие, S – программный оператор, а ψ – постусловие.

Тройка {φ} S {ψ} известна как тройка Хоара [13] и названа в честь

одного из пионеров в области формальной верификации

компьютерных программ. Существуют две интерпретации троек

Хоара в зависимости от того, частичная или тотальная корректность

рассматривается.

 Формула {φ} S {ψ} называется частично корректной, если каждое

останавливающееся вычисление S, стартующее в состоянии, в

котором выполняется φ, финиширует в состоянии, в котором

выполняется ψ.

 Формула {φ} S {ψ} называется тотально корректной, если каждое

вычисление S, стартующее в состоянии, в котором выполняется φ,

останавливается и финиширует в состоянии, в котором

выполняется ψ.

Таким образом, в случае частичной корректности не делается никаких

предположений относительно вычислений S, которые не

останавливаются, а зависают. В дальнейших объяснениях

рассматривается частичная корректность, если не сказано обратное.

Основная идея подхода Хоара – доказывать корректность программ на

синтаксическом уровне, используя лишь тройки определенной выше

формы. Детерминированные последовательные программы

конструируются по следующей грамматике:

S ::= skip | x := E | S; S | if B then S else S fi | while B do S od.

Здесь skip – отсутствие операции, x := E – присваивание выражения E

переменной x (предполагается, что x и E имеют одинаковый тип), S; S

– композиция операторов. Последние два – альтернатива и итерация,

соответственно (B – булево выражение).

Правила вывода должны читаться следующим образом: если все

условия, расположенные выше черты, верны, тогда следствие под

чертой тоже верно. Для правил с условием true записывается только

следствие. Эти правила вывода называются аксиомами. Формальная

система для последовательных детерминированных программ

изображена в табл. 1.1.

Таблица 1.1. Формальная система для частичной корректности

последовательных программ

Аксиома для skip

   



skip

Аксиома для присваивания

 

 

::x k x k





Последовательная композиция

       

   

;

   



Альтернатива

       

   

B S B S

B S S

   



  

if then else fi

Итерация

   

B S B





while do od

Следствие

   

,,' ' S ' '

     





Правило вывода для оператора skip, который ничего не делает, вполне

ожидаемо: при любых условиях, если φ верно перед оператором, то

оно верно и после него.

В соответствии с аксиомой для присваивания, начинают с

постусловия φ и определяют предусловие подстановкой φ[x := k]. Эта

подстановка означает формулу φ, в которой во всех вхождениях x

заменено на k. Например,

четно и k = y} x := k {x

четно и x = y}.

Если процесс доказательства начинается с анализа постусловия, то его

обычно применяют последовательно к частям программы таким

образом, что в конце можно доказать предусловие для всей

программы.

Правило последовательной композиции использует промежуточный

предикат χ, который характеризует финальное состояние S

стартовое состояние S

Правило альтернативы использует булево выражение B, значение

которого определяет, что именно исполняется: S

или S

Правило для итерации требует пояснения. Оно определяет, что

предикат φ выполняется после окончания while B do S od, если

справедливость φ может быть поддержана в течение каждого

исполнения тела цикла S. Это объясняет, почему φ называется

инвариантом. Одна из основных трудностей в доказательстве

правильности программ с помощью рассматриваемого подхода

состоит в нахождении подходящих инвариантов. В частности, это

усложняет автоматизацию таких доказательств.

Все рассмотренные правила ориентированы на такой синтаксис, что

каждой синтаксической конструкции соответствует правило вывода.

Это отличается от правила следствия, которое устанавливает связь

между верификацией программ и логикой.

Правило следствия позволяет усиливать предусловия и ослаблять

постусловия. При этом оно облегчает применение остальных правил.

В частности, это правило позволяет заменять пред- и постусловия

эквивалентными. Тем не менее, следует отметить, что доказательство

импликаций вида φ  φ' в общем случае неразрешимо.

Теперь обсудим тотальную корректность. Системы доказательств в

табл. 1.1 недостаточно для доказательства того, что последовательная

программа останавливается. Единственная синтаксическая

конструкция, которая может вести к зависающим (не

останавливающимся) вычислениям, – это итерация. Для

доказательства наличия останова можно усилить правило вывода для

итерации следующим образом:

       

   

, , 0

B S B n N S n N n

B S B

   



      

while do od

Здесь вспомогательная переменная N не входит в φ, B, n или S. Смысл

этого правила заключается в том, что N является стартовым значением

n, и на каждой итерации значение n уменьшается, но остается

неотрицательным. Эта конструкция в точности ликвидирует

бесконечные вычисления, так как n не может уменьшаться бесконечно

часто без нарушения условия n ≥ 0. Переменная n называется

вариантой.

Формальная верификация параллельных систем

Пусть для операторов S

и S

конструкция S

|| S

обозначает

параллельную композицию этих операторов. Основным для

применения формальной верификации к параллельным программам

является следующее правило вывода:

       

   

S ' S '

' S S '

   

   



Это правило позволяет верифицировать параллельные системы тем же

путем, что и последовательные, рассматривая части программ по

отдельности. Ввиду взаимодействия между S

и S

хотя бы за счет

доступа к разделяемым переменным или обмена сообщениями, это

правило, к сожалению, в общем случае неверно. Много усилий было

приложено к получению правил вывода описанной формы [14].

Существует несколько причин, почему достичь этого непросто.

Введение параллелизма по существу приводит к введению

недетерминизма. Это означает, что для параллельных программ,

которые взаимодействуют путем использования разделяемых

переменных, поведение на входе-выходе существенно зависит от

порядка, в котором к этим общим переменным получен доступ.

Например, если S

– это x := x + 2, S

– это x := x + 1; x := x + 1 и S

–

это x := 0, значение x после выполнения S

|| S

может быть 0 или 2, а

значение x после выполнения S

|| S

может быть 0, 1 или 2. Различные

значения для x зависят от порядка выполнения операторов в S

и S

или S

и S

. Более того, несмотря на то, что входное-выходное

поведение S

и S

идентично (увеличение x на 2), нет никакой

гарантии, что это будет верно в параллельном контексте.

Параллельные процессы потенциально могут взаимодействовать в

любой момент их исполнения, а не только в начале вычисления. Если

требуется сделать вывод о том, как параллельные программы

взаимодействуют, недостаточно знать свойства их стартовых и

финальных состояний. Необходимо также уметь формировать

суждения о том, что происходит во время вычисления. Таким образом,

свойства должны ссылаться не только на стартовые и финальные

состояния, но и на сами вычисления.