2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 15

Считал, что сигналы на выходе этой схемы стабилизировались, на этом вычислении (назовем епз и ) можно интерпретирошпь (определить нстинностное значение) любую формулу БП. с атомарными предикатами р и' 0. В часпкютн, для этой схемы выполняются следующие свойства: П п)=рС р: на вычисяении и когда-нибудь а будущем сигнал р сбросится н останется в этом сброшенном сосговнни; ьз п~ РСл: когда-нибудь в будущем сигнал л установится и останется в этом состоянии постоянно; О пНС(р сь 0): в любом состоянии если установлен сигнал р, то и сигнал с установлен; гэ п~=рВ( рл 0): оба сигнала, р и л, когда-нибудь в будущем будут сброшены, а до этого сигнал 0 будет все время установлен. Последнее свойство выполняется на вычислении и, потому что оно выполняется в начальном состоянии п(0) этого вычисления.

Действительно, оба сипшла, р н 0, в соегоянии п(З) будут сброшены, а во всех предыдущих состояниях, о(2) и(1) и п(0), сигнал д установлен. Формулы ПЪ могут служить лля задания множеств бесконечных цепочек гтак называемых е-языковй Например, формула (а ч Ь) Ю(СЬ) щлает асе бесконечные цепочки из а и Ь, содерясащие только конечное число вхвкдений сммеола а (подробнее этот вопрос рассматриеаетсв в ак Е. 2.7. Соотноаьения между операторами ).Т(. Будем говорить, что две темпорвльные формулы ф и р логики ЬТ1. эквиваленшы, и писать фвф, если они выршкмот одно и то же свойство бесконечных вычислений. Инымн слоаамн, <рвЧ~ означает, чзп для любого вычисления и утверждение ц! ц вернотогдантолькотогда, когда п~ ц верно.

м,а жно Операторы Ц, У н С можно опредеянзь бесконеенымв формуламн о по. мощью оператора Х: р5о ейч(рлХР)ч(рлХрлХХР)ч... Ро меч У»Г»УГКЦ ч ХХХо ... Ср мел Хр лХХлл ХХХб „. Можно определить зтн операторы рекурснвно, сама через себя (рнс. 2,1 !): рбо меч (рл Х(рПР)) Ро в лч ХРо Совал ХОР Зтн определения яснм н без формального доказательства. аны выо. нг яв в!ге е» в лхбяаб .. о в Р Р Р а ГЕ а»ХРас ае елхоес е а е а е а е о Рлс. ЗЛ !.

Резурснвное опреаеленне темпсраяьнмз опершеров Приведем несколько соотношений, которые легко м б огуг ыть доказаны на основании формального определеншг семантики формул !Л$.. Комбвввнвв темпоралвныз операторов в булевыл онерацвйг Х(рчр)мХР»ХР Х(рл р) н ХрлХР Хр Х-"р р(рч д) м рр ч ро сп С(рлб) мСрлСР хгмее 2 (рпд)С и'р«)глд()г' р%(дчг) и рЪ3дч рПг Законы поглощенна (ндемпатвпжееть)г ккр кр ССриСр р()(р)зд) рЬд (рПд)Вд ирПд КСКр СКр СКС р и КСр Существует множество других соотношений межау операторамн ЬТЬ. Например, общезначимые (всегда истинные) тхпношення: Ср ~ Кр — "то, что всегда будет, то когда-нибудь ностуниий р иь Кр — "то, что есть, то когда-нибудь наступив«". (Срч Сд)уг«С ( р ч д) — "еслн всегда будет и«ленино р или всегда будет нстинно д, то всегда будет истинно род". С(р ~д) иь (Ср и«Сд) — "если наступление р всегда влечти наступ- ление д, то если р будет истинно всегд«х то н д будет истинно всел)а'.

2.8. Структура Крипке Выбор подходящей математической модели является важнейшим этапом в исследовании объектов н явлений реального мира. Для исследованию поведения реагирующих систем такой молелью являетса структура Кринке. По заданному вычислению — бесконечной леночке состояний с определенным в кткдом состоянии набором атомарных предивное, истинных в этом состоянии, мы определяли значения истинности булевых н темпоральных «рормул. Как такие вычисления представить конечным обриюмд В качестве модели, которая конечным образом представляет бесконечные поведения, удобно выбрать систему переходов.

Даже если система переходов имеет конечное число состояний, в общем случае количество в«зноя«ных вычислений в ней бесконечно и юпкдое вычисление также бесконечно. Например, одно бесконечное вычисление (см. рнс. 2.$) может быль представлено конечной снсюмой переходов (рис. 2.12, б), поскольку поспешны союжжпне вычислещм бесконечно повтораегся. На- Рнс. 2:12. Структура Кринке (а), одно из ее вычислений (б) н се рвзаерпа — дерево вмчнслеинй (а) Мы згиаем в линейном мире: после сегодняшнего дня будет завтра, потом послезавтра.и т.

п. В логике (.Т(. формализован именно этот взгляд на време, как на линейную последовательность дискретных возрастмощих значений (в частности. состояния любого вмчисленна можно пронумеровать натуральнмм рядом). Однако в жизни каждого человека встречмотся точки вепшения, когда внешние события, принятые решения или выполненные действия могут направить жизнь либо по одному. либо по другому пути. Хотя у кажлого есть возмшкности таких изменений, но ревлизуетса только одна конкретная линия лопни нз многих возмоюгых. Поведения реальных информационных систем также имеют альтернативы, выбор которых осуществляется на основе внешних собьггнй, рвшичнй в содерэжнин принятых сообщений и т. п. Поэтому в общем случае конкретное вычисление технической дискретной системы — лишь одно нз многих воз- ~е о Гласе 2 и т1 Пр Вь 1ы дм Мн ножных ее вычислений.

Нв рис. 2.12, а ярелстаялена модель системы переходов с конечным числом соспмний. Одно нз ее вычислений показано на рнс. 2.4 н 2йх На рис, 2,12, е показано дерево всех возмвкных вычислений модели 2.12, а — ее разверни. Для формаеьного задания таких систем переходов используется модель, которал назыеасгся "смруюгброй Крняяе", Струкгура Кринке имеет конечное множество сосгояннй и (непомеченных) переходов между ними, причем каждое состояние помечено множеством истинных в этом состоянии атомарных преди юнов.

Ф Определение 28 сги ' 'л авр Структура Кринке М вЂ” это пятерка М (Я, сс, Я, АР, Е), где: ° 'Я вЂ” конечное непустое множество состояний; ° бе ~ Я вЂ” непустос множество начальных состояний; ° Я~ухо — тотальное отношение иа Я, т. е. множество переходов, удоаястеоряюжее требованию: (тз вб)(Зз'и Я)(зз) ел (из любого состояния есть перехол); ° АР— конечное множество атомарных преднквмж; ° Е: Я -+24~ — функция пометок (кюккому состоянию отсбрюкенне Е сопостаияяет множество истинных в нем атомарных предикатовф Рис.

2.12, а задаст структуру Кринке с четырьмя состояниями (зб,з1,з2,4З», одним начальным состоянием 40, множеством атомарных предикатов (Р,р,г» нфункниейпомсток Е: Е(зб)=(РО», Е(Н)=(д,г», Е(з2)=(г», Е(зЗ)=(» . Ф 2.В Гвычислвиив слг умп К ппкв! Вычислением струкгуры Кринке М называется любая бесконечная цепочка пр Вес~Огсз..., такал, что Освус и (Он йь,)ед. Формально вычисление струкгуры Кринке М макно предспвигь как огобралиние а: ДГ-+Я, где Дà — множество натуральных чисел, т. е. и(1) — это некопзрое состояние структуры Кринке. Одно из вычислений структуры Кринке рис. 2.12, а — зб зЪ з1 з2 з2зЗ ....

т1 бл л ра В ко В ере> на ний ко- 2.10 Р Траекторией структуры Кринке М, н иду цироващюй вычислениемнием и = де р> дз д> ... называется бесконечная цепочка ь(п) Ь(йс)Е(р>)ЬЙ2)Ь(сэ).„, т.е. бесконечная >ыпочка подмио. жеста атомарных предикатов, истинных в соответствующих состояниях вычисления и. Формально, траекгорнв — зто отображение натурального ряда в мнщкество 2"г. дов, >бо- :ние >в). >ЗЦ пов г), ~ьно ыие Траекторией структуры Кринке рис.

2.12, а при вмчислении эб зЗ з1з2 з2зЗ... является следующая цепочка: (р,сЦ ЦщгЦгЦг(.... Траектории структуры Кринке иногда называют трассами. Траектории являются последовательностями подмножеств атомарных преднкатов — наблюдаемых свойств (щ>бьпнй, соотношений между переменными н т. п.), которые могут выполниться (произойти) в анализируемых системах. Именно эти последовательности ящщются важными дяз аналищ. Формулы темпо- ральной логики описывают свойства траекторий.

В структуре Кринке в кмкдом состоянии указаны атомарные преднкаты из конечного мнщкеспа АР атомарных предиззтов, которые истинны (выщщняются) в этом состоянии. Кщкдое такое подмножество атомарнмх предика>он можно считать символом, помечвющнм состояние структуры Кринке. В теории формальных языков конечные цепочки, построенные над конечным словарем, называются словами, а бесконечные цепочки назыввкжя и-озонами. Кщкдвв траектория струкгуры Кринке является бесконечной. Поэтому траектории структуры Кринке называются также ее м.словами. Пример 2гй Вычисления, показанные на рис. 222, е индуцнруют следующие траектории (и-слова) — бесконечные цепочки подмнщяаств мнщкества в>омарных преликатов, которые выполняются в последовательно проходимых состояниях: я> =(р,йЦФгЦгЦ )..; кз (.Р ч (ч гЦг)(г)". яз --(р,рЦ ЦщгЦгЦ )...; к4 (Р >)Ц > (т г> (гЦг> Мнекас>во всех и словлтрукзу)м> Крнщю М называется а языком, допус- каемым М.

Т2 Глвев 2 Итак, в отличие от конечного автомата, кшгдое состояние сгрукгуры Кринке помечено некоторым миояиством атомарных утверждений, истинных в этом состоянии. Структуру Кринке можно считать расширением конечного автомата, в котором отсутствуют пометки на переходах, поскольку цель структуры Кринке — задать конечным образом бесконечные логледаеаюкгьности состояний (вычисления) при произвольных входах, В структуре Кринке мы не рассматриваем причины переходов — конкретные внешние события, существенные в модели конечного авюмата. Такие события легко могут быть учтены в модели Кринке, но при верификации иам чаще всего важно проверить, существует ли некоррекпюе поведение сисшмм при любых последовательноспш внешних событий, и только когда такое некорректное поведение найдено, мы можем искать и его причину.

Например, верификация системы управления медицинского прибора облучения Тйегас-25 должна была гарантировать, что прн всех возможных нажатиях его кнопок медицинским персоналом прибор не смшает войти в режим, в котором инзенсивность облучения пациента превышаю бы заданную границу. Друюй пример: разработчики бортовой системы управления советских межпланегных станций "Фобос-1" и "Фобос-2" должны были гарантировать, что любые случайные последовательности команд с Земли не приведуг систему в неуправляемое состояние, в котором отключены системы стабилизации, ориентации и свези.

Тотальность множества переходов означает, что нз каждого состояния существует хотя бы один переход. Если моделируемая система останавливается в каком-либо завершающем состоянии, то в соответствующей ей модели— структуре Кринке — указывается переход в то же самое состояние. Таким образом, струкгура Кринке, все вычисления каторой бесконечны, может опу,шить моделью и завершжошихся вычислений. Структура Кринке валяется семантической моделью реагирующих систем.

Логические системы управлеииа, протоколы коммуникации и параллельные взаимодействуюигне программы — все зти системы достаточно адекватно могут быль представлены структурой Кринке (си. гл, от. Поскольку при анализе реагирующих систем нас интересуют бесконечные вычисления и соответствующие им траектории (а-слова), то все состояния структуры Кринке мшкно считать принимающими состояниями в том смысле, что любое е.слово, которое индуцнруигсв каким-либо вычислением структуры Крипке М, будет допускаться М. Главным достоинством этой простой модели — структуры Крипке — является возможность конечным образом задавать поведения дискретных систем: бесконечное число бесконечных вычншшний н нидуцнрованных нми трешь торий.