Семинар 4. NuSMV_ композиция автоматов_ проверка CTL-формул
Описание файла
PDF-файл из архива "Семинар 4. NuSMV_ композиция автоматов_ проверка CTL-формул", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016НапоминаниеКакую задачу мы решали в последних лекциях?Широкая формальная постановкаДаныIмодель Крипке M = (S, S0 , R, L)ICTL-формула ϕТребуется вычислить множество состоянийSϕ,M = {s | s ∈ S, M, s |= ϕ}aaa, b∅НапоминаниеКакую задачу мы решали в последних лекциях?Узкая формальная постановкаДаныIмодель Крипке M = (S, S0 , R, L)ICTL-формула ϕТребуется проверить выполнимость формулы ϕ в модели M:?S0 ⊆ Sϕ,M , или?M |= ϕaaa, b∅НапоминаниеКакую задачу мы решали в последних лекциях?Содержательная постановкаДаныIнеформальное описание системыIсодержательное описание требований к системеТребуется проверить,удовлетворяет ли система набору требованийСистемаТребованияПрограмма-максимум — научить вас решать такую содержательно поставленную ЗАДАЧУСхема решения ЗАДАЧИописание системыописание требованийформализациямодель Крипке MCTL-формула ϕалгоритм проверки CTL-формул?M |= ϕСхема решения ЗАДАЧИописание системыописание требованийформализациямодель Крипке MIдля некоторых классов систем можно придумать алгоритмтрансляции в модели КрипкеIIIICTL-формула ϕпрограммы со строгой семантикойкомбинационные и последовательные схемы(схемы из функциональных элементов с задержкой)...в общем случае нет никаких ограничений на способыописания системы, а значит, нет и единообразныхспособов формализации системыСхема решения ЗАДАЧИописание системыописание требованийформализациямодель Крипке MCTL-формула ϕIтребования обычно формулируются на естественном языкеIтот, кто предъявляет требования к системе, часто неможет точно сказать, чего он хочетIформализация требований — отдельный долгий икропотливый процессСхема решения ЗАДАЧИмодель Крипке MCTL-формула ϕалгоритм проверки CTL-формул?M |= ϕКак только модель и формула получены, процесс проверкистановится абсолютно бездумнымВы уже знаете два основных алгоритма проверки соотношенияM |= ϕ:Iтабличный алгоритмIсимвольный алгоритмА какой алгоритм разумнее реализовывать в средствеверификации?Средства верификацииТабличный алгоритм нагляден и лежит в основе всех другихалгоритмов, но неэффективен: чем больше модель Крипке,тем медленнее она будет обрабатыватьсяСимвольный алгоритм менее нагляден, но намного болееэффективен:IIоснова символьного алгоритма — преобразование и анализбулевых функцийпрограммистский арсенал содержит средства эффективнойработы с большими булевыми функциями:IIIбиблиотеки для работы с ROBDDSAT/SMT-решатели...Как правило, в средствах верификации используетсясимвольный алгоритм, насыщенный разнообразнымиоптимизациями и эвристикамиА насколько популярен model checking для CTL в средепрограммистов?Средства верификацииВот список программных средств, способных проверятьвыполнимость CTL-формул в каких-то моделях:(на случай если захотите их использовать)ARCBANDERACADENCE SMVCWB-NCExpander2GEARLTS-minMCMASNuSMVProBTAPAsDisclaimer: список скорее всего неполный, и я не знаю большинства этихсредств; информация взята из соответствующей страницы в википедииВ курсе сосредоточим внимание на средстве NuSMV:Iоно открытое и бесплатноеIоно довольно популярноIего язык достаточно прост для пониманияСинтаксис NuSMV: модулиСистема в NuSMV описывается как композиция модулей:MODULE <имя модуля >(<аргументы >) <тело модуля >Модуль — это описаниенедетерминированного конечного автоматаБлок с аргументами модуля может быть опущен вместе соскобкамиВид и назначение аргументов будут описываться дальше, асейчас полагаем, что их нетИмя модуля, как и все имена, — это непустая строка изсимволов A..Za..z0..9_$#−, начинающаяся с одного изсимволов A..Za..z_Все компоненты описания автомата, которые будут показаныдальше, — это элементы тела модуляСинтаксис NuSMV: типы данныхПространство состояний модуля образовано (если коротко)декартовым произведением областей переменных,используемых при описании модуляТипы переменных:Iboolean: значения TRUE и FALSEIinteger: значения от INT_MIN + 1 до INT_MAX; это те жемашинно-зависимые константы, что и в C/C++{val1 , .
. . , valk }: перечисление (enumeration); vali — либочисло, либо имяIIв частности, integer — это перечисление особого видаСинтаксис NuSMV: типы данныхПространство состояний модуля образовано (если коротко)декартовым произведением областей переменных,используемых при описании модуляТипы переменных:Iunsigned word[i], где i > 0: беззнаковые числа с битовойзаписью ширины iIsigned word[i], где i > 0: знаковые числа с битовойзаписью ширины iarray i..j of T, где i, j — константы и T — тип: массивэлементов типа T с индексацией от i до jIIпри определении массивов допускается вложенность,например, array 0..2 of array 3..7 of booleanNuSMV умеет (немного, но всё же) приводить типы(читайте про это в документации или постигайте практикой)Синтаксис NuSMV: пространство состоянийПространство состояний модуля описывается так:VAR<имя > : <тип >;<имя > : <тип >;...Пример:MODULE birdVARsatiety : {FED, HUNGRY, DEAD};flying : boolean;Так описывается автомат с шестью состояниями:(FED, FALSE)(FED, TRUE)(HUNGRY, FALSE)(HUNGRY, TRUE)(DEAD, FALSE)(DEAD, TRUE)Синтаксис NuSMV: начальные состоянияМножество начальных состояний модуля — это конъюнкцияINIT-выражений такого вида:INIT <выражение >;Точку с запятой можно опускать (здесь и в других аналогичныхместах)<выражение > — это выражение типа boolean, построенное надпеременными модуляСледует запомнить, что все выражения в NuSMV — этоформулы, даже если в них встречается равенствоНапример, запись вида “a = b” часто используется приописании систем в NuSMV, но означает не “обычное”последовательное присваивание, а формулу, истинную тогда итолько тогда, когда значения a и b совпадаютСинтаксис NuSMV: выраженияЧто точно можно использовать при построении выражений:IконстантыIIIIIбулевого типа: TRUE, FALSEцелочисленного типа: 0, 1, -1, .
. .символьного типа: все имена, использовавшиеся вперечисленияхинтервального типа: i..j, где i, j — целочисленныеконстанты; значение — множество целых чисел от i до jword-типа: целочисленное значение в двоичной (b),восьмеричной (o), десятичной (d) либо шестнадцатеричной(h) системе счисления в особом формате, например:II0ub5_10011 или 0b_10011 — беззнаковая константаширины 5, описывающая число 190so_77 — знаковая константа ширины 6, описывающаячисло −1Синтаксис NuSMV: выраженияЧто точно можно использовать при построении выражений:Iимена переменныхIскобки, как обычно в формулахIбулевы и побитовые операции: ! (отрицание), &, |, xor,xnor, ->, <->Iарифметические (и где возможно, также булевы) операциии отношения: +, -, *, /, mod, <, <=, >, >=, =, !=, abs(...)(модуль), max(..., ...), min(..., ...)Iоперации над битовыми векторами: » (сдвинуть вправо), «(сдвинуть влево), :: (конкатенация)Iоперации индексирования: ...[e] (e-й элемент массива,e-й бит слова), ...[e1:e2] (подслово слова от бита e1 добита e2Синтаксис NuSMV: выраженияЧто точно можно использовать при построении выражений:Iоперации над множествами: union, in, {e1, .
. . , ek}(множество из k элементов), e1..e2 (интервал от e1 доe2)Iусловное выражение: e ? e1 : e2case-выражение: case <выражение > : <выражение >;<выражение > : <выражение >; . . . esacIIIII...просматриваются пары <выражение > : <выражение > впорядке следованиявыбирается первая пара, левое выражение которойистиннорезультат case-выражения — правое выражение этой парыСинтаксис NuSMV: начальные состоянияПримерMODULE birdVARsatiety : {FED, HUNGRY, DEAD};flying : boolean;INIT ! (satiety = DEAD);INIT flying = TRUE | flying = FALSE;Так описывается множество из четырёх начальных состояний:(FED, FALSE)(FED, TRUE)(HUNGRY, FALSE)(HUNGRY, TRUE)Вторая строка с INIT избыточна, она здесь только для того,чтобы показать, что разрешено писать несколькоINIT-выраженийСинтаксис NuSMV: переходы автоматаСовокупность переходов автомата определяется конъюнкциейTRANS-выражений:TRANS <next-выражение>;Next-выражение отличается от обычного выражения тем, что внём могут встречаться записи вида next(<имя переменной >)<имя переменной > — это значение переменной до выполненияпереходаnext(<имя переменной >) — это значение переменной послевыполнения переходаПодобные выражения уже встречались в лекциях раньше: влекции 3 рассказывалось, как описывать отношения переходовс помощью формул, используя два комплекта переменных(“штрихованный” и “нештрихованный”)next(<имя переменной >) — это штрихованная версияпеременной (в нотации лекции 3 )Синтаксис NuSMV: переходы автоматаПримерMODULE birdVARsatiety : {FED, HUNGRY, DEAD};flying : boolean;INIT ! (satiety = DEAD);TRANS satiety = FED -> next(satiety) = HUNGRY;TRANS satiety = HUNGRY ->next(satiety) in {HUNGRY, DEAD};TRANS satiety = DEAD ->next(satiety) = DEAD & !next(flying);И какие же переходы описываются такой совкупностьюTRANS-выражений?Синтаксис NuSMV: переходы автоматаTRANS satiety = FED -> next(satiety) = HUNGRY;TRANS satiety = HUNGRY ->next(satiety) in {HUNGRY, DEAD};TRANS satiety = DEAD ->next(satiety) = DEAD & !next(flying);(FED, FALSE)(HUNGRY, FALSE)(DEAD, FALSE)(FED, TRUE)(HUNGRY, TRUE)(DEAD, TRUE)Синтаксис NuSMV: переходы автоматаTRANS satiety = FED -> next(satiety) = HUNGRY;TRANS satiety = HUNGRY ->next(satiety) in {HUNGRY, DEAD};TRANS satiety = DEAD ->next(satiety) = DEAD & !next(flying);(FED, FALSE)(HUNGRY, FALSE)(DEAD, FALSE)(FED, TRUE)(HUNGRY, TRUE)(DEAD, TRUE)Синтаксис NuSMV: переходы автоматаTRANS satiety = FED -> next(satiety) = HUNGRY;TRANS satiety = HUNGRY ->next(satiety) in {HUNGRY, DEAD};TRANS satiety = DEAD ->next(satiety) = DEAD & !next(flying);(FED, FALSE)(HUNGRY, FALSE)(DEAD, FALSE)(FED, TRUE)(HUNGRY, TRUE)(DEAD, TRUE)Синтаксис NuSMV: переходы автоматаTRANS satiety = FED -> next(satiety) = HUNGRY;TRANS satiety = HUNGRY ->next(satiety) in {HUNGRY, DEAD};TRANS satiety = DEAD ->next(satiety) = DEAD & !next(flying);(FED, FALSE)(HUNGRY, FALSE)(DEAD, FALSE)(FED, TRUE)(HUNGRY, TRUE)(DEAD, TRUE)А почему новые переходы объединялись с построеннымиранее, несмотря на то что по семантике множество переходовописывается конъюнкцией выражений?Синтаксис NuSMV: переходы автоматаДругой примерMODULE birdVARsatiety : {FED, HUNGRY, DEAD};flying : boolean;TRANS satiety = HUNGRY;Так тоже можно писать в NuSMVПохожа ли эта система на ненасытную бессмертную птицу?Как будет выглядеть модель Крипке и почему?MODULE birdVARsatiety : {FED, HUNGRY, DEAD};flying : boolean;INIT satiety = HUNGRY;TRANS satiety = HUNGRY;А здесь всё хорошо?ПрисваиванияНередко при описании систем в NuSMV используются блоки,напоминающие последовательность присваиваний:ASSIGN<имя переменной > := <выражение >;init(<имя переменной >) := <выражение >;next(<имя переменной >) := <выражение >;...Как работает “v := e;”:(точнее описано в документации)Iесли выражение имеет тип переменной, то это работаеткак “TRANS v = e”(всё чуть иначе — см.