4. NuSMV - обзор средства.

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 4NuSMV(обзор средства)Задача model checkingШирокая формальная постановкаДаныIмодель Крипке M = (S, S0 , R, L)Iтемпоральная формула ϕТребуется вычислить множество состоянийSϕ,M = {s | s ∈ S, M, s |= ϕ}aaa, b∅Задача model checkingУзкая формальная постановкаДаныIмодель Крипке M = (S, S0 , R, L)ICTL-формула ϕТребуется проверить выполнимость формулы ϕ в модели M:?S0 ⊆ Sϕ,M , или?M |= ϕaaa, b∅Задача model checkingСодержательная постановкаДаныIнеформальное описание системыIсодержательное описание требований к системеТребуется проверить,удовлетворяет ли система набору требованийСистемаТребованияПрограмма-максимум — научиться решать такуюсодержательно поставленную ЗАДАЧУЗадача model checkingНа всех оставшихся семинарах ЗАДАЧА будет решаться припомощи программных средств верификацииКаждое из этих средств принимает на вход систему итребования, описанные на специальном языке,Iдостаточно понятном, чтобы можно было легко описыватьбольшие системы и сложные требования к нимIдостаточно строгом, чтобы можно было легкопереформулировать это описание как задачу modelchecking в узкой формальной постановке (проверить,выполняется ли формула на модели Крипке)Схема решения ЗАДАЧИсистематребованияформализациямодель Крипке Mформула ϕалгоритм model checking?ответ на вопрос M |= ϕСхема решения ЗАДАЧИсистематребованияформализациямодель Крипке MCTL-формула ϕалгоритм model checking для CTL?ответ на вопрос M |= ϕНа ближайших семинарах будет рассматриваться логикаветвящегося времениСхема решения ЗАДАЧИмодель Крипке MCTL-формула ϕалгоритм model checking для CTL?ответ на вопрос M |= ϕВам известно (как минимум) два алгоритма проверкиCTL-формул:I табличный алгоритмIIIIнаглядный и понятныйлежит в основе всех других алгоритмовкрайне неэффективныйсимвольный алгоритмIIненаглядный и не очень понятныйнамного эффективнее табличного (?)Схема решения ЗАДАЧИмодель Крипке MCTL-формула ϕсимвольный алгоритм model checking для CTL?ответ на вопрос M |= ϕЭффективность символьного алгоритма зависит отэффективности средств работы с булевыми функциямиТаких средств в программистском арсенале огромноемножество, и обычно такое средство — это одно из двух:1.

библиотека для работы с BDD2. средство проверки выполнимости булевых и иных формул:SAT/SMT-решательСредство верификации, как правило, содержит полнуюреализацию алгоритма, так что“применение алгоритма верификации” =“применение средства верификации согласно инструкции”Схема решения ЗАДАЧИсистематребованияформализациямодель Крипке Mформула ϕКак правило, система и требования формулируются наестественном или полуформальном языкеФормализация системы и требований как модели Крипке иформулы темпоральной логики (или как описание на входномформальном языке средства верификации) — этонетривиальный процесс, требующий немалой квалификацииИменно этому процессу будут посвящены все оставшиесясеминарыА может, никто так не делает,и вообще верификация CTL никому не нужна?Схема решения ЗАДАЧИВот список программных средств, способных проверятьвыполнимость CTL-формул в каких-то моделях:(на случай если захотите их использовать)ARCBANDERACADENCE SMVCWB-NCExpander2GEARLTS-minMCMASNuSMVProBTAPAsDisclaimer: список неполный, и я не знаю большинства этих средств;информация взята из соответствующей страницы в википедииВ курсе сосредоточим внимание на средстве NuSMV:Iоно открытое и бесплатноеIоно довольно популярноIего язык достаточно прост для понимания(ν) Hello, World!···(ν) МодулиМодуль — это описание модели Крипке и предъявляемых к нейтребованийПервая строка модуля с именем name (без параметров)выглядит так:MODULE nameДопустимые имена в NuSMV состоят из символов“A-Za-z0-9_$#-” и начинаются с “A-Za-z_”Для ясности записью M[m] будем обозначать модель Крипке,описываемую модулем mГлавный модуль называется main и не содержит параметров, иименно для него проверяются требования утилитой NuSMV(ν) ПеременныеСостояние M[md] (в простом случае), — это совокупностьзначений всех переменных, объявленных в md при помощиключевого слова VAR:VAR объявление ; объявление ; ...

объявление ;объявление ::= имя : типboolean — это тип с множеством значений {TRUE , FALSE }Модель M[main] имеет два состояния:b/FALSEb/TRUE(ν) Начальные состоянияНачальные состояния модели M[md] — это все состояния,удовлетворяющие каждой формуле в описании md,записанной под ключевым словом INITФормула — это любое выражение (simple expression) типаboolean над переменными, объявленными в mdЕсли бы в модуле main не было строки 3, то каждое состояниемодели M[main] было бы начальным:b/FALSEb/TRUEС учётом строки 3 модель M[main] содержит ровно одноначальное состояние:b/FALSEb/TRUE(ν) ПереходыДля описания множества переходов модели M[md]используется два комплекта переменных:1.

переменные, объявленные в mdIими обозначаются значения переменных в текущемсостоянии модели (начальные значения)2. переменные вида next(x),где x — переменная, объявленная в mdIIими обозначаются значения переменных в следующемсостоянии модели (конечные значения)переменную next(x) будем называть next-аналогомпеременной x(ν) ПереходыNext-формула — это next-выражение (next-expression) типаboolean, то есть выражение над переменными модуля и ихnext-аналогамиПереход содержится в модели M[md] ⇔начальные и конечные значения перехода удовлетворяюткаждой next-формуле, записанной под ключевым словомTRANS(ν) ПереходыЕсли бы в модуле main не было строки 4, то модель M[main]выглядела бы так:b/FALSEb/TRUEС учётом строки 4 модель M[main] выглядит так:b/FALSEb/TRUE(ν) СпецификацииТребования, предъявляемые к модели M[md], записываютсянепосредственно в модуле mdНас будут интересовать требования, записанные в видеCTL-формулТакие требования записываются под ключевым словом CTLSPECБНФ, определяющая синтаксис CTL-формул (Φ):Φ ::= формула | (Φ) | !Φ | Φ & Φ | “Φ | Φ” |Φ xor Φ | Φ xnor Φ | Φ -> Φ | Φ <-> Φ |AXΦ | EXΦ | AGΦ | EGΦ | AFΦ | EFΦ |A[ΦUΦ] | E[ΦUΦ](вроде бы синтаксис довольно естественныйи пояснений не требует?)(ν) Типы данныхIбулев тип: boolean, значения — {TRUE , FALSE }Iперечисление, или множество: {val1 , .

. . , valk }, где vali —число или имяIинтервал: i..j — это множество целых чисел от i до jвключительно, где i и j — константные выраженияцелые числа с двоичной записью ширины i:IIIIбеззнаковые: unsigned word [i]знаковые: signed word [i]массивы: array i..j of T, это набор переменных типа T,индексируемых от i до j включительноIв том числе вложенные массивы, например,array 0..2 of array 3..7 of boolean(ν) КонстантыIконстанты типа boolean: TRUE, FALSEIцелочисленные константы: 0, 1, 2, .

. .(их можно использовать не везде)Iсимвольные константы: имена, встречающиеся вперечисленияхword-константы в одной из обычных систем счисления:двоичной (b), восьмеричной (o), десятичной (d),шестнадцатеричной (h) — записываются в особомформате:III0ub5_10011 и 0b_10011 — число 19 в 5-ти битах0so_77 — число −1 в 6-ти битах(ν) ВыраженияВыражения строятся в условиях статической типизации снебольшими возможностями приведения типов (о которыхможно почитать в документации) надIконстантами, объявленными переменными, скобкамиInext-аналогами объявленных переменных (дляnext-выражений)Iбулевыми операциями: !, &, |, xor, xnor, ->, <->Iарифметическими операциями: +, -, *, /, mod, abs(),max(,), min(,)Iарифметическими отношениями: <, <=, >, >=, =, !=Iпобитовыми операциями: <<, >>, :: (конкатенация)Iоперациями индексирования: [i] (элемент массива),[i:j] (подслово слова)(ν) ВыраженияВыражения строятся в условиях статической типизации снебольшими возможностями приведения типов (о которыхможно почитать в документации) надIоперациями для множеств: {e1 , .

. . , ek }, union, in, e1..e2Iтернарным оператором: ?:Iоператором выбора:case альтернатива ; ... альтернатива esacIIII...альтернатива ::= формула : выражениевыбирается первая по прочтению альтернатива, значениеформулы которой — TRUEрезультат — значение выражения выбранной альтернативы(ν) Композиция модулейМожно описывать системы, состояющие из многих модулейИмя модуля можно использовать в качестве типа переменнойОбъявленная так “переменная” — это экземпляр модуля,участвующий в синхронной композиции: при совершенииперехода главный модуль и все объявленные экземплярыодновременно совершают переходДоступ к локальным переменным модуля выглядит так же, какдоступ к полям структуры в C/C++(ν) Композиция модулейМодель M[main] выглядит так:b/TRUEm.b/TRUEb/TRUEm.b/FALSEb/FALSEm.b/TRUEb/FALSEm.b/FALSE(ν) МакроопределенияОбъявление макроопределения выглядит так:DEFINE имя := выражение ;Вместо имени макроопределения во всех местах модуляподставляется соответствующее выражениеЗначение макроопределения не входит в состояние модели(ν) МакроопределенияМодель M[main] выглядит так:b/TRUEc/TRUEb/TRUEc/FALSEb/FALSEc/TRUEb/FALSEc/FALSE(ν) Модули с параметрамиОписание модуля может содержать параметры — имена,перечисленные в скобках через запятую после имени модуляВнутри модуля параметр работает примерно какмакроопределение:I имя макроопределения — это имя параметра;I тело макроопределения в конкретном экземпляре — этоnext-выражение, записанное на соответствующем месте вобъявлении экземпляра(ν) Модули с параметрамиМодель M[main] выглядит так:n.b/TRUEs.b/TRUEn.b/TRUEs.b/FALSEn.b/FALSEs.b/TRUEn.b/FALSEs.b/FALSE(ν) Инвариант состоянийИногда бывает удобно описать общее устройство модели ипосле этого сказать:“из всего, что я описал, в модели остаются только состояния,удовлетворяющие формуле ϕ,и переходы между этими состояниями”Такое ограничение множества состояний записывается так:INVAR ϕ;Записанное так ограничение ϕ добавляется ко всем остальнымограничениям в описании модуля как для переменных, так идля их next-аналогов(ν) Инвариант состоянийМодель M[main] содержит ровно одно состояние:b/TRUE(ν) Специальные переменныеСтабильная переменная определяется так же, как и обычная,но с ключевым словом FROZENVAR вместо VARСтабильная переменная — это переменная, значение которойопределяется в начальном состоянии системы и больше неизменяетсяБолее точно:Iзначение стабильной переменной присутствует в состояниимоделиIзапрещено писать выражения, в которых говорится, какимдолжно быть значение стабильной переменной послепереходаIнеявно предполагается ограничение TRANS next(x) = x;для каждой стабильной переменной x(ν) Специальные переменныеВходная переменная определяется так же, как и обычная, но сключевым словом IVAR вместо VARВходная переменная — это переменная, значениями которойразмечаются переходы из каждого конкретного состоянияБолее точно:Iзначение входной переменной не является составнойчастью состояния моделиIвходные переменные не могут встречаться в видеnext-аналогов и в формулах, не относящихся к переходамIвходные переменные могут встречаться в TRANS, и в TRANSописываются ограничения не только на начальные иконечные переменные состояния, но и на значения входныхпеременных(ν) Специальные переменныеМодель M[main] выглядит так:b/0i/2i/2i/1i/1i/1b/1b/2i/2(ν) ASSIGNКлючевое слово ASSIGN используется для единообразнойзаписи распространённых видов ограничений:I ASSIGN переменная := выражение равносильноIIIASSIGN init(переменная ) := выражение равносильноIIIINVAR переменная in выражение , если значениевыражения — множествоINVAR переменная = выражение в противном случаеINIT переменная in выражение , если значениевыражения — множествоINIT переменная = выражение в противном случаеASSIGN next(переменная ) := next-выражениеравносильноIITRANS next(переменная ) in next-выражение , еслизначение выражения — множествоTRANS next(переменная ) = next-выражение впротивном случае(ν) Асинхронная композицияВ NuSMV версии 2.6.0 поддерживаются, но считаютсяустаревшими встроенные средства асинхронной композициимодулей (согласно семантике чередующихся вычислений)При выполнении заданий разрешается использовать этисредства, однако для понимания того, как именно их следуетприменять, следует внимательно прочитать документациюАсинхронная композиция модулей может быть организованапри помощи синхронной:Iв каждом экземпляре есть параметр “твой ход”Iесли “твой ход” = TRUE, то экземпляр изменяет своёсостояние, иначе сохраняет текущие значенияIвнешний модуль (или специальный экземпляр) выступаетв роли арбитра: определяет очерёдность ходов(ν) Асинхронная композицияМодель M[main] выглядит так:i/2m1.b/TRUEm2.b/TRUEi/1 i/1m1.b/FALSEm2.b/TRUEi/2i/2i/2m1.b/TRUEm2.b/FALSEi/1 i/1m1.b/FALSEm2.b/FALSE(ν) СправедливостьНапоминание, лекция 4: ограничения справедливостиIIделят все пути модели Крипке на справедливые инесправедливыеизменяют семантику кванторов пути:IIAϕ = “для любого справедливого пути верно ϕ”E ϕ = “существует справедливый путь,для которого верно ϕ”(ν) СправедливостьНапоминание, лекция 5: классический способ заданияограничения справедливости для CTL выглядит так:Iэлементарное ограничение — это множество состояниймодели КрипкеIпуть справедлив относительно элементарного ограничения⇔ хотя бы одно из состояний ограничения встречается внём бесконечно частоIограничения справедливости — это множествоэлементарных ограниченийIпуть справедлив относительно ограниченийсправедливости ⇔ он справедлив относительно каждогоэлементарного ограничения(ν) СправедливостьJUSTICE формула ; — это классическое элементарноеограничение справедливости для CTL:Iпуть модели M[main] справедлив ⇔ формула каждогоограничения JUSTICE, записанного в main илипорождаемого в main объявленными экземплярами,истинна в бесконечно многих состояниях этого путиIкаждым ограничением JUSTICE ϕ(x1 , .