WWW.KNIGA.LIB-I.RU
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - Онлайн материалы
 

«Опубликовано в Научно-техническом вестнике СПбГУ ИТМО. 2008. Выпуск 53. Автоматное программирование, с. 137-145. УДК 004.4’242 ВЕРИФИКАЦИЯ ПРОГРАММ, ...»

Опубликовано в Научно-техническом вестнике СПбГУ ИТМО. 2008. Выпуск 53. Автоматное программирование, с. 137-145.

УДК 004.4’242

ВЕРИФИКАЦИЯ ПРОГРАММ, ПОСТРОЕННЫХ НА ОСНОВЕ

АВТОМАТНОГО ПОДХОДА С ИСПОЛЬЗОВАНИЕМ

ПРОГРАММНОГО СРЕДСТВА SMV

Е.А. Курбацкий

(Санкт-Петербургский государственный университет информационных технологий, механики и оптики)

В работе рассматривается метод верификации программ, построенных на основе автоматного подхода c использованием метода проверки на моделях (Model Checking). Для проверки модели используется программное средство SMV. При предлагаемом подходе система переходов не строится в явном виде, что позволяет верифицировать программы с большим числом состояний.

Ключевые слова: верификация программ, верификация на моделях, автоматное программирование Введение В работе [1] описан метод верификации программных систем, основанный на моделях (Model Checking). При использовании этого метода строится система переходов с конечным числом состояний. Свойства модели выражаются на языке темпоральной логики, после чего проверяется соответсвие модели свойствам. Одной из основных проблем методов Model Checking является необходимость построения конечной модели для проверки. Эта процедура может быть весьма сложной, а построенная в результате модель может обладать огромным числом состояний, что затрудняет верификацию.



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

При использовании автоматного программирования [2] проблема, указанная выше, решается на этапе проектирования программы. В автоматной программе все состояния разделены на два класса [3] – управляющие и вычислительные. При этом управляющие состояния описываются набором конечных автоматов. Набор взаимодействующих автоматов уже является моделью, которая адекватна автоматной программе. Эта модель имеет конечное число состояний, что является необходимым условием для ее верификации.

Данная проблема рассматривалась в ряде работ. В работе [4] описан способ проверки одного автомата. В работе [5] приводится способ проверки системы автоматов.

При этом предлагается использовать программное средство SPIN [6].

Постановка задачи Рассматривается задача проверки свойств программы, построенной на основе автоматного подхода [2]. Существует большое число программ, реализующих алгоритмы верификации моделей. В данной работе предлагается использовать программное средство SMV (Symbolic Model Verifier) [7]. Верификатор SMV предназначен для проверки того, что система переходов удовлетворяет требованиям, заданным на языке ветвящейся темпоральной логики CTL. В верификаторе SMV применяется описанный в работе [1] символьный алгоритм верификации моделей, основанный на упорядоченных двоичных диаграммах решений (Ordered Binary Decision Diagram – OBDD).

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

Таким образом, задача сводится к следующим подзадачам:





преобразовать программу в модель на языке SMV;

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

запустить программу-верификатор SMV;

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

На рис. 1 изображена схема предлагаемого подхода.

–  –  –

Построение модели выполняется в два этапа.

1. Так как система переходов допускает пометки только в вершинах, то для каждого автомата строится модель автомата. Вводятся дополнительные состояния на переходах, которые соответствуют действиям, выполняемым автоматом на переходах.

2. Полученные модели автомата объединяются в одну систему переходов и записываются как переменные и правила переходов между ними на языке SMV.

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

Промежуточное состояние автомата фиксируется каждый раз, когда автомат совершит одно из следующих действий:

вызовет выходное воздействие, при этом в состоянии указывается, какое выходное воздействие вызывается;

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

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

Состояниями модели автомата будут состояния исходного автомата и промежуточные состояния. Условие и событие, записанные на переходе автомата, записываются на переходе модели из основного состояния в промежуточное. Промежуточные состояния нумеруются так, чтобы начальное состояние автомата имело номер 0. На рис. 2 приведен пример выделения промежуточных состояний для одного перехода.

s1

–  –  –

Рассмотрим задачу преобразования нескольких моделей автоматов в систему переходов. Состояние модели будет описваться набором переменных. Каждому автомату

Ak сопоставим переменную Statek. Для всей системы автоматов в целом введем переменные Active, Event, xk (0 k m), где m – число входных переменных. Введенные переменные имеют следующий смысл:

переменная Statek содержит состояние модели, в котором может находиться каждая из n моделей. Каждая переменная может принимать значения от нуля до количества состояний модели;

переменная Active содержит номер автомата, активного в данный момент, или ноль, если никакой автомат не активен;

переменная Event содержит имя события, которое передано автомату в данный момент. Событие может быть передано от внешнего источника или от другого автомата в результате вызова. Если в данный момент никакое событие не передается, то переменная Event принимает значение ноль;

переменные x1, x2, xm... соответствуют входным воздействиям. Каждая переменная может принимать значения ноль (ложь) или один (истина).

Каждое состояние модели представляет собой объединение переменных Statek (1 k n), Active, Event, xk (0 k m). Так как состояние задается набором переменных, то можно не строить систему переходов в явном виде. Таким образом, можно проверять модели с большим числом состояний.

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

Зададим начальное значение всех переменных:

переменные Statek для всех k содержат состояния модели, соответствующие начальным состояниям всех автоматов;

переменная Active содержит ноль;

переменная Event содержит ноль;

переменные x1, x2,... xm содержат входные воздействия, которые могут принимать значения ноль или единица.

Теперь зададим правила переходов. Для Statek запишем следующие правила переходов:

если автомат активен (Active = k), то изменение значения переменной Statek выполняется в соответствии с переходами модели автомата k. Переменная Statek может изменить свое значение на любое значение, в которое есть переход из текущего состояния в модели автомата, если условие, записанное на переходе, выполняется;

если никакой переход невозможен, значение переменной Statek не изменяется;

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

Опишем изменение значения переменной Active. Возможно несколько вариантов:

если переменная Active равна нулю, то никакой автомат в данный момент времени не активен, а, следовательно, требуется выбрать автомат, который будет выполняться. Этот выбор происходит недетерминировано из множества всех номеров автоматов. После того, как автомат для выполнения выбран, его номер записывается в переменную Active;

иначе переменная Active равна k. Это значит, что активен автомат k. Для определения значения переменной Active необходимо рассмотреть следующее состояние модели k. Это состояние содержится в переменной Statek;

если состояние Statek – промежуточное состояние, и в нем вызывается автомат l, следовательно, он будет активен на следующем шаге. Таким образом, переменной Active необходимо присвоить значение l;

если Statek является состоянием исходного автомата, следовательно, автомат k уже закончил переход. Проверим, нет ли автомата l, который вызвал автомат k;

если автомат l был вызван каким-то другим автоматом m, то управление требуется вернуть к автомату m. Следующее значение переменной Active будет равно m;

иначе следующее значение переменной Active равно нулю;

иначе значение переменной Active не изменяется.

Переменная Event принимает следующие значения:

если переменная Active равна k, и следующее значение переменной Statek соответствует вызову автомата с событием e, то следующее значение переменной Event равно e;

иначе следующее значение Еvent равно нулю.

Преобразование системы автоматов в модель для SMV

Опишем преобразование моделей автоматов в модель на SMV. Каждая модель автомата размещается в отельном модуле с именем, соответсвующим имени автомата.

Каждый модуль будет иметь следующие параметры:

Active – является ли данный модуль активным;

Event – входящее событие, переданное автомату;

Ap1, Ap2,... – состояния экземпляров автоматов, с которыми данный модуль взаимодействует.

x1, x2,... – входные воздействия.

Определение модуля имеет следующий вид:

MODULE name(Active, Event, Ap1, Ap2, …, x1, x2, … xm) Каждый модуль будет хранить номер текущего состояния модели в переменной State. Она описывается State: 0..p;. Здесь p – число состояний модели данного автомата.

Далее требуется указать правила, по которым будут изменяться значения переменных. Эти правила описываются в секции ASSIGN.

Вначале значение переменной State = 0. Это записывается как init(State) = 0; Для каждого состояния модели указывается, в какие состояния модель может переходить. Это делается при помощи ключевого слова TRANS, после него записывается предикат, истинность которого означает наличие перехода. Чтобы составить такой предикат, запишем условия для каждого перехода, объединив их операцией логического или.

Для каждого перехода из состояния si в состояние sj, который происходит по событию eij при условии cij, записывается:

(Active & State = si & next(State) = sj & Event = eij & cij) | Для каждого состояния модели si запишем условие того, что ни один переход из данного состояния не возможен.

(Active & State = si & next(State) = si & !(Event = ei1 & ci1) & !(Event = ei2 & ci2) &...) | Если автомат не активен, то состояние не изменяется.

(!Active & State = next(State)) Далее требуется выразить основные состояния автоматов. Это записывается в секции DEFINE:

DEFINE s1 := State = n1;

s2 := State = n2;

...

Далее выразим свойство, что модель находится в состоянии автомата:

inState := State = n1 | State = n2 | …;

Здесь s1, s2,... – имена состояний автомата, а n1, n2,... – соответствующие им номера состояний модели.

Переменные, общие для всей системы, записываются в модуле main после ключевого слова VAR:

переменные xk, описывающие входные воздействия, записываются как xk: {0, 1};

переменные, описывающие экземпляры автоматов записываются как name:

name(Active = k, Event, Ap1, Ap2, …, x1, x2, … xm), где name – имя автомата k, Ap1, Ap2 – имена автоматов, с которыми он взаимодействует, x1, x2,..., xm – входные воздействия;

переменная Event описывается следующим образом:

Event: {0, e1, e2, e3, …}.

–  –  –

Для записи требований используются формулы темпоральной логики ACTL.

Опишем, как записываются свойства автоматной модели в виде формул ACTL.

Введем формулы, которые будут описывать состояния автоматов:

для записи условия, что автомат Ak находится в состоянии sj, достаточно записать Ak.sj;

условие того, что выполнилось выходное воздействие z1, записывается как z1;

для записи условия, что произошло событие ei, достаточно записать Event = ei;

Для записи формул, описывающих состояния автомата, также можно использовать логические операторы.

Если f и g – формулы состояния, то формулами состояния являются:

f & g – одновременно выполняются f и g;

f | g – выполняется либо f либо g;

f xor g – выполняется либо f либо g, но не одновременно;

!f – не выполняется f;

f - g – если выполняется f, то выполняется g;

f - g – тоже что и (f - g) & (g - f).

Помимо свойств текущего состояния, в условиях можно использовать темпоральные операторы: AF, AG, AU. Оператор AX не используются для записи свойств автоматов, так как в данной модели один переход автомата соответствует неопределенному числу переходов модели.

Опишем эти операторы:

AF f (Future) – оператор будущего. Означает, что на всех путях из текущего состояния существует состояние, когда формула f выполнитсяЯ;

AG f (Global) – оператор означает, что данная формула f будет выполняться на каждом пути из текущего состояния в каждом состоянии: f будет выполняться в каждом состоянии, достижимом из текущего состояния;

A[f U g] (Until) – оператор истинен, только если на каждом пути когда-нибудь выполнится формула g, а до этого момента всегда будет выполняться формула f.

Преобразование контрпримера

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

Каждое состояние является набором переменных Event, Statek, Active, xk (0 k m). Предлагается следующий алгоритм для преобразования контрпримера к системе переходов в контрпример к системе автоматов. Контрпример к системе автоматов также представляется в виде последовательности состояний, только вместо значений переменных информация предоставляется в терминах состояний и действий. Для каждого состояния контрпримера выведем следующую информацию о системе автоматов.

Если Active = 0, то никакой автомат не активен. Данное состояние не учитывается в контпримере для автомата.

Если Active != 0, то выводится название активного автомата. Также выводится действие активного автомата. Выводятся состояния всех автоматов, полученые из переменных Statek. Аналогично выводятся значения всех входных воздействий, записанных в переменные xk, и значение переменной Event.

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

Продемонстрируем построение модели на небольшом примере. Рассмотрим два потока, которым необходимо время от времени работать с некоторым ресурсом. При этом необходимо, чтобы в каждый момент времени только один из потоков мог иметь доступ к ресурсу, но не оба сразу. Для моделирования этого примера, потребуются три автомата. Автомат A0 будет соответствовать ресурсу, а автоматы W1 и W2 - потокам.

На рис. 3 изображена диаграмма переходов автомата A0.

Рис. 3. Автомат A0

Автомат имеет два состояния:

unlocked – начальное состояние означает, что ни один из потоков не использует ресурс. Автомат переходит из этого состояние в состояние locked по событию lock;

locked – это состояние означает что ресурс в данный момент используется. Автомат переходит из этого состояния по событию unlock в состояние unlocked.

На рис. 4 приведена диаграмма переходов автомата W1. Автомат W2 устроен аналогично. Изначально оба автомата находятся в состоянии wait. После этого один из них переходит в состояние work, в котором он может вызывать выходное воздействие z1.

По окончанию работы по событию e1 автомат возвращается в состояние wait.

На рис. 5 приведены модели автоматов A0 и W1.

Похожие работы:

«И. З. Шкурченко Энергетическая структура Солнца и планет солнечной системы с точки зрения механики безынертной массы Работа "Энергетическая структура Солнца и планет солнечной системы с точки зрения механики безынертной массы" (1977) является прямым продолжением работы "Строение Солнца и пла...»

«RU 2 428 170 C2 (19) (11) (13) РОССИЙСКАЯ ФЕДЕРАЦИЯ (51) МПК A61K 8/97 (2006.01) A61Q 19/00 (2006.01) A61Q 19/08 (2006.01) ФЕДЕРАЛЬНАЯ СЛУЖБА ПО ИНТЕЛЛЕКТУАЛЬНОЙ СОБСТВЕННОСТИ, ПАТЕНТАМ И ТОВАРНЫМ ЗНАКАМ (12) ОПИСАНИЕ ИЗО...»

«Юлия Николаевна Улыбина Сергей Николаевич Бердышев Искусство управления складом Tекст предоставлен правообладателем www.iprmedia.ru http://www.litres.ru/pages/biblio_book/?art=172186 Аннотация Настоящее практическое пособие по ск...»

«ВЕСТНИК ТОМСКОГО ГОСУДАРСТВЕННОГО УНИВЕРСИТЕТА 2014 Математика и механика № 1(27) УДК 539.319 М.А. Осипенко КОНТАКТНАЯ ЗАДАЧА ОБ ИЗГИБЕ ДВУХЛИСТОВОЙ РЕССОРЫ С ЛИСТАМИ ПЕРЕМЕННОЙ ТОЛЩИНЫ Рассмотрена контактная задача об изгибе двухлистовой рессоры с односторонним контактом листов перем...»

«Ученые записки Таврического национального университета им. В. И. Вернадского Серия "Юридические науки". Том 23 (62). № 2. 2010 г. С. 282-291. ТРИБУНА МОЛОДОГО УЧЕНОГО УДК 343.85 МЕЖДУНАРОДНЫЕ МЕХАНИ...»

«Министерство образования и науки Российской Федерации Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования "Ярославский государственный технический университет" ПРОГРАММА КАНДИДАТСКОГО ЭКЗАМЕНА по сп...»

«БЕЛОРУССКИЙ НАЦИОНАЛЬНЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ УДК 539.3 + 612.311 ЮРКЕВИЧ Кирилл Сергеевич БИОМЕХАНИЧЕСКОЕ МОДЕЛИРОВАНИЕ НАПРЯЖЕННО-ДЕФОРМИРОВАННОГО СОСТОЯНИЯ СИСТЕМЫ ЗУБ–ПЕРИОДОНТ ПРИ ОРТОДОНТИЧЕСКОМ ЛЕЧЕНИИ Автореферат дисс...»

«HANSA Кондиционер HAP 09 H Руководство пользователя Перед эксплуатацией внимательно прочтите настоящее руководство пользователя Содержание Меры предосторожности..3 Технические характеристики..3 Детали изделия..4 Аксессуары..5 Панель управления..6 Рекомендации по эксплуатации..7 Пульт ДУ..9 Кн...»

«Рустем ВалееВ Нетрадиционные алгоритмы для логистических задач ООО "Островитянин" УДК 519.7+519.87 ББК 65.291.592 В15 Валеев Р. Ч.В15 Нетрадиционные алгоритмы для логистических задач. – СПб.: Островитянин, 2012. – 160 с. ISBN 978-5-98921-048-0 Рустем...»

«Приборы ультразвуковые УКС – МГ4 УКС – МГ4С Руководство по эксплуатации* Основные технические и метрологические характеристики _ * Сокращенная версия РЭ. Предназначена для ознакомления. Некоторые разделы отсутствуют. Приборы ультразвуковые УКС-МГ4 (УКС-МГ4С) СОДЕРЖАНИЕ 1 ОПИСАНИЕ И РАБОТА ПРИБОРА 1.1 Назначение и область применения 1...»








 
2017 www.kniga.lib-i.ru - «Бесплатная электронная библиотека - онлайн материалы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.