7. Обзор средства SPIN - синтаксис, трансляция базовых конструкций в модели Крипке

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 7Spin(обзор средства)Рассматриваемая ЗАДАЧАДаныIнеформальное описание системыIсодержательное описание требований к системеТребуется проверить,удовлетворяет ли система набору требованийСистемаТребованияСхема решения ЗАДАЧИсистематребованияформализациямодель Крипке Mформула ϕалгоритм model checking?ответ на вопрос M |= ϕСхема решения ЗАДАЧИсистематребованияформализациямодель Крипке MLTL-формула ϕалгоритм model checking для LTL?ответ на вопрос M |= ϕНа ближайших семинарах будет рассматриваться логикалинейного времениСхема решения ЗАДАЧИмодель Крипке MLTL-формула ϕалгоритм model checking для LTL?ответ на вопрос M |= ϕВам известно (как минимум) два алгоритма проверкиLTL-формул:I табличный алгоритмIIIIнаглядный, хотя и не такой понятный, как для CTLлежит в основе всех других алгоритмовкрайне неэффективныйавтоматный алгоритмIIболее сложно устроенныйнамного эффективнее табличного (?)Схема решения ЗАДАЧИмодель Крипке MLTL-формула ϕавтоматный алгоритм model checking для LTL?ответ на вопрос M |= ϕЭффективность автоматного алгоритма model checking для LTLобеспечивается двумя составляющими:1.

эффективно работающее представление автоматов Бюхи2. эффективный алгоритм поиска компонент сильнойсвязности, достижимых из входов автоматаВ программном средстве LTL-верификации, как правило,эффективно реализована вариация автоматного алгоритмаСхема решения ЗАДАЧИсистематребованияформализациямодель Крипке Mформула ϕЭтап формализации модели и требований по-прежнемуостаётся и мало чем отличается от того, что происходило насеминарах, посвящённых CTLА может, никто так не делает,и вообще верификация LTL никому не нужна?Схема решения ЗАДАЧИВот список программных средств, способных проверятьвыполнимость LTL-формул в каких-то моделях:(на случай если захотите их использовать)BANDERACADENCE SMVLTSALTSminNuSMVPATProBSALSATMCSPINSpot...Disclaimer: список неполный, и я не знаю большинства этих средств;информация взята из соответствующей страницы в википедииНекоторые из этих средств работают и с CTLВ курсе сосредоточим внимание на средстве Spin:Iоно открытое и бесплатноеIоно довольно популярноIего язык (Promela: Process meta language) достаточнопрост для понимания(и намного более приятен, чем язык NuSMV )(S) Hello, World!На этом примере можно разобрать основы того,Iкак описывать желаемые модели Крипке на языке PromelaIкак применять средство средство Spin для верификацииLTL-формулМногие конструкции языка Promela схожи с такими жеконструкциями C/C++ и/или NuSMV как по синтаксису, так ипо семантике (вплоть до того, что некоторые части C/C++-кодаможно особенным образом вставлять в модель Promela, но этивозможности в обзоре не обсуждаются)(S) Модель Крипке: состоянияВ примере объявлена одна глобальная переменная b типа boolЭта переменнаяIможет принимать два значения: 0 и 1, они же false иtrue соответственноIинициализируется значением 0(S) Модель Крипке: состоянияВ примере описан один тип процесса (~объект/функция вC/C++, ~модуль в NuSMV)Описание типа процесса имеет следующий вид:proctype тип_процесса (аргументы ) {тело_процесса }(S) Модель Крипке: состоянияСистема на каждом шаге работы содержит некоторое числозапущенных процессовКаждый процессIзаданным образом последовательно изменяетпеременные системы согласно описанию в теле типапроцессаIна каждом шаге работы системы имеет текущее состояниеуправления: значение счётчика команд, указывающее накоманду, которая должна выполниться следующей(S) Модель Крипке: состоянияКлючевое слово active перед типом процесса означает, что вначале работы запускается один процесс этого типаСостояние управления запускаемого процесса — это перваякоманда в теле процессаСостояние модели Крипке, соответствующей системе на языкеPromela, в числе прочего содержитIтекущие значения всех глобальных переменныхIтекущие состояния управления всех запущенных процессов(S) Модель Крипке: состоянияМодель Крипке для этого примера имеет два состояния, средикоторых ровно одно начальное:b/0b/1Состояния управления процессов будут опускаться виллюстрациях моделей для краткости и наглядности(S) Модель Крипке: переходыПеременные изменяются совокупностью параллельноработающих процессов согласно семантике чередующихсявычисленийВ частности, если в системе запущен один процесс, то онIв рамках перехода выполняет следующую командуIесли выполнил все команды, то может завершиться(исчезнуть из системы)(S) Модель Крипке: переходыЕдинственный процесс, запущенный в примере,Iвыполняет безусловный бесконечный цикл do-odIна каждом витке цикла выполняет присваивание значения!b в переменную bCемантика языка устроена так, что в данном примере одинвиток цикла выполняется за один переход в модели Крипке, тоесть после каждого перехода счётчик команд указывает наначало цикла(S) Модель Крипке: переходыМодель Крипке для этого примера выглядит так:b/0b/1(S) Язык LTL-формулОписание системы включает в себя список проверяемыхLTL-свойствОписание свойства располагается вне тел всех процессов ивыглядит так:IIltl имя_свойства { тело_свойства } — дляименованных свойствltl { тело_свойства } — для безымянных свойствIбезымянное свойство рекомендуется использовать только втом случае, если оно одно во всей системе(S) Язык LTL-формулБНФ, описывающая синтаксис LTL-свойств (ϕ):ϕ::=булево_выражение | ϕ && ϕ | “ϕ || ϕ” | !ϕ |ϕ -> ϕ | ϕ implies ϕ | ϕ <-> ϕ | ϕ equivalent ϕ[] ϕ | always ϕ | <> ϕ | eventually ϕ |ϕ U ϕ | ϕ until ϕОперацияимпликацияGUВ БНФ->, eventually[], alwaysU, untilОперацияравносильностьFXВ БНФ<->, equivalent<>, eventuallyотсутствуетИспользование средства SpinСпособ 1: консоль Linux1.

По исходному тексту модели получить исполняемый файлверификатораИспользование средства SpinСпособ 1: консоль Linux2а. Запустить верификатор с флагом “проверь это свойство” иубедиться, что свойство выполненоИспользование средства SpinСпособ 1: консоль Linux2б. Запустить верификатор с флагом “проверь это свойство” иубедиться, что свойство не выполненоИспользование средства SpinСпособ 2: GUI ispinispin — это графическая оболочка от разработчиков Spin,написанная на tcl/tkИспользование средства SpinСпособ 2: GUI ispinispin — это графическая оболочка от разработчиков Spin,написанная на tcl/tkИспользование средства SpinСпособ 3: GUI jspinjspin — это сторонняя графическая оболочка, написанная наJavaИспользование средства SpinСпособ 3: GUI jspinjspin — это сторонняя графическая оболочка, написанная наJava(S) Простые типы данныхМногие встроенные типы данных, имеющиеся в Promela,аналогичны типам с теми же названиями в CIbool: значения 0 и 1, они же false и trueIbit: синоним boolIbyte: значения — целые числа от 0 до 255Ishort: значения — целые числа от −215 − 1 до 215 − 1Iint: значения — целые числа от −231 − 1 до 231 − 1unsigned: беззнаковые числа, хранящиеся в заданномчисле бит, явно указываемом при объявленииIIunsigned x : 5 = 2; — объявление беззнаковогопятибитового числа x с начальным значением 2(S) Непростые типы данныхIразрешено объявление одномерных массивов, и выглядитэто так же, как и в C, с поправкой на инициализацию:IIbyte state[4] = 1; — объявление массива state из 4-хэлементов типа byte, каждый из которыхинициализируется числом 1typedef — это ключевое слово, аналогичное struct в C:IItypedef T {bool a; int b;}; — тип T с двумя полямиtypedef onedim {bool a[4];}; — “костыль”,позволяющий работать с многомерными массивами(S) Непростые типы данныхIперечисление: mtype = {имена_через_запятую }IIаналогично enum в C с некоторыми поправкамитип перечисления всегда один, и это тип mtypeIIImtype x; — объявление перечисляемой переменной xнесколько перечислений “сливаются” в одно записьюперечисляемых имён в порядке следования в текстенумерация перечисляемых объектов начинается с 1, тоесть перечисляемая переменная инициализируетсязначением 0, отличающимся от всех числовыхэквивалентов перечисляемых имёнРемарка: “mtype” = “message type”; изначальное назначение типа mtype —перечисление типов сообщений в каналах связи между процессами; но mtypeможно использовать и в других целях, а о каналах будет рассказано дальше(S) Непростые типы данныхПримерmtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Здесь объявленыIIпеременная symvar, которой можно присаивать значенияA, B, C, D, E, Fмассив twodim, содержащий три элемента типа T:Iкаждый элемент содержит массив a из пяти булевыхзначений(S) Композиция процессовКаждая команда в теле процесса описываетнедетерминированный способ изменения состояния системы:выполнение команды соответствует одному, нескольким или ниодному переходу в модели КрипкеВ последнем случае команда и процесс, содержащий этукоманду, считаются заблокированными в текущем состоянии, аиначе — активнымиШаг выполнения системы (переход в модели Крипке) выглядиттак:Iнедетерминированно выбирается активный процессIнедетерминированно выполняется следующая командапроцессаЕсли Spin применяется согласно инструкции, то в случае, когдавсе процессы заблокированы, в систему добавляется переход,при выполнении которого состояние системы не изменяется(S) Композиция процессовМодель Крипке в примере выглядит так:b1/0, b2/0b1/1, b2/0b1/0, b2/1b1/1, b2/1(S) Тело процессаКак и в C, каждая команда может быть предварена меткой:имя_метки : командаТело процесса содержит последовательность команд,разделённых “;”, включающуюIприсваиванияIусловияIветвленияIциклыIкоманду goto(S) Тело процесса: присваиваниеПрисваивания выглядят примерно так же, как и в C с сильноограниченным синтаксисом:имя = выражениеимя ++имя --(S) Тело процесса: присваиваниеВ выражениях используются переменные, константы (целыечисла, true, false, имена перечисления) и многие операторы,аналогичные C, например:I+, -, *, /I<<, >>, ~, &, ^, |I<, >, <=, >=, ==, !=I!, &&, ||I->: (аналог ?:), [] (индексирование массивов),.