Подходы к верификации моделей

Объектная модель и модель распределенного приложения отражают специфику предметной области и принципы взаимодействияобъектов со средой функционирования. Их верификации посвящен ряд работ, в том числе [6.22]. Эта область верификации требует дальнейшего развития и в рамках международного проекта на ближайшие десятилетия будет одним из главных ее направлений.
Верификация объектных моделей основывается на спецификации следующих элементов:
1. Базовых (простых) объектов ОМ, атрибутами которых являются данные и операции объектфункции над этими данными.
2. Проверенных объектов с помощью операций (функции), используемых в качестве теорем, а все операции, которые применяются над их подобъектами, не выводят их из множества состояний объектов.
3. Верифицированных интерфейсов объектов путем доказа тельства правильности передачи типов и количества данных в пара метрах сообщений, заданных в языке IDL. Интерфейс состоит из операций обращения к объекту, который посылает данные другому объекту через сообщение.
Для доказательства правильности спецификации сообщения создается набор утверждений, доказывающий, что для любой пары элементов сообщения, например, и , переход от к проходит за один шаг. Действие, выполняемое в промежутке между и , приводит к . При этом часть утвердждений проверяет входной параметр и его поступление на вход другого объекта в целях подтверждения его на выходе. Если доказано, что объект, инициированный сообщением, формирует правильный выходной результат - выходной параметр, то сообщение считается правильным.
Доказательство правильности построения ОМ для некоторой ПрО состоит в следующем:
· вводятся дополнительные и/или удаляются лишние атрибуты объекта и его интерфейсов в ОМ, доказывается правильность объекта ОМ после изменений спецификации интерфейсов и взаимодействий с другими объектами;
· доказывается правильность задания типов для атрибутов объекта, т.е. подтверждения того, что выбранный тип реализует операцию, а множество его значений определено на множестве состояний этого объекта;
· доказывается правильность спецификации объектов ОМ и параметров интерфейсов, которые передаются другим объектам.Этим заканчивается заключительное доказательство проверки правильности ОМ.
Верификация модели распределенного приложения - это спецификация процессов SDL (Spesification Description Language), задание модели проверки (model-checking) и индуктивных утверждений. Метод предложен новосибирской школой программирования в [6.12, 6.13]. В нем проверки состоит в редукции системы с бесконечным числом состояний к системе с конечным числом состояний, а также в доказательстве распределенных приложений с помощью индуктивных рассуждений и системы переходов конечного автомата.
Связь между процессами распределенного приложения осуществляется через специальный канал, который передает сообщение с параметрами или без них в качестве сигнала. В него поступает запись после освобождения или чтения очередного сигнала. Процесс задается последовательностью действий, приводящих к изменению переменных, чтению сигнала из канала, записи в канал и очистке канала. Проверка спецификации ограничивается условиями справедливости.
Основные типы данных спецификации в SDL - предопределенные и конструируемые типы данных (массив, последовательность и т.д.). Формулы описываются с помощью предикатов, булевых операций, кванторов, переменных и модальностей. Семантика их определения зависит от последовательных действий (поведений), спецификацией процесса и от момента времени их выполнения.
В предикатах используются локаторы управляющих состояний процессов, контроллеры заполнения каналов (пусто/заполнен канал), а также отношения между переменными и параметрами сигналов. Спецификация процесса состоит из заголовка, контекста, схемы и подспецификации. В заголовке указывается имя и вид процесса, формулы или предикаты.
Контекст - это описание типов, переменных и каналов. Переменная принадлежит процессу, если в ее описании указано место и имя процесса (через точку), которому эта переменная принадлежит. При ее использовании указывается имя переменной с расширением. Если указывается параметр, то в расширенное имя входит имя канала, сигнал и имена параметров, разделенных точками.
В логических условиях используются кванторы всеобщности и существования.
Схема спецификации процесса - это описание условий выполнения и диаграмм процессов. Она инициируется посылкой сообщения во входной канал, который передает сообщение внешней среде для выполнения.
Диаграмма процесса состоит из описаний переходов, состояний, набора операций процесса и перехода на следующее состояние. Набор операций - это действия типа: чтение сообщения из входного канала, запись его в выходной канал, очистка входного и выходного каналов, изменение значений переменных программы Рпроцесса.
Каждая операция определяет поведение процесса и создает некоторое событие. Логическая формула задает модальность поведения спецификации и моменты времени. Процесс, представленный формальной спецификацией, выполняется недетерминировано. Обмен с внешней средой производится через входные и выходные параметры сообщений.
Событие. В каждый момент времени выполнения процесс имеет некоторое состояние, которое может быть отражено в виде снимка, характеризующего это событие, и включает в себя значения переменных, которым соответствуют параметры и характеристики состояний процесса. К событиям процесса относятся:
· отправка сообщения в канал;
· получение сообщения из канала;
· чистка входных и выходных каналов;
· выполнение программ;
· анализ непредвиденного события (взлом канала и др.).
Семантика выполнения процесса определяется в терминах событий и правил с помощью следующего типа утверждения:
любой процесс вызывает событие при чтении или записи сообщения из/в канал, а также при выполнении процесса в узле распределенной системы.