2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 71
Текст из файла (страница 71)
Щ Неислвивпгаи точка еиервтера тгд (2) = Я, < ЕХ(2) определяется так: это яюбое мне<застал состоаний А, включающее только такие состояния нз множества Се, из которых за одия июг можно достичь состояний из А. (Щ Семаитвиа формулы ЕСф определяется так: это все такие состояния, на которых формула <р выполняется и из которых существует (бесконечный) путь, во всех состояниях которого формула ф выполияетсж Мозно вилл<э, что определение неподвюкной точки оператора тк (Е) более слабое, чем семантическое определение: в нем отсутствует информация о семантике формулы ЕС<р и следующем нз нее аягоригме построения множества Окп .
Попому определению неподвижной точки оператора тко мо<уз удовлепоря<ь и те множества состояннй, которые не являются решением наше релю (пуст тичь Инту< вижн може ний— го фа Прин ки мо ритм< харак форм лодзь вычи< Крин< ской < Гм х' < Прим Рассм творя< гоств тког( Яде< ее го нашей проблемы.
Например, пустое мпожеспю ю удовлепюряст зиму определеиию: опо вовсе ие включшт состояний из Д и поэтому включает (пустое) миожеспю всех тех ссстояиий, из которых за один шаг макио достичь состояний из И. Очевидно, что Ы вЂ” зто наименьшая иеподвюкшш точкаоператора ткс (2)=Я,гэЕХ(У). юро. вы- ищем Интуитивно ясно, что искомое множество Око яшшстся наибольшей иеподвижиой точкой оператора ткп и, следовательно, по теореме Тарского, оно мшкег быть найдена простым алгоритмом последовательных приблихмиий — "аппроксимацией сверху": подсчетом т"ап (Я).
Доказательспю этого факта аналогично доказательству Леммы 10.13. Приведем симжиьиый алгоритм вычислению наибольшей неподвижной точки монотонного оператора тко (с) = Я, /э ЕХ(У), который и шшяепж алгоритмом верификации для подформулы ЕС~р. Этот алгоритм манипулирует характеристическими булевыми функциями множеств, представленными в форме ВОО и полностью аналогичен алгоритму вычисления наименьшей неПОДВИжНОй ТОЧКИ ОПЕРатОРа ткс, ПРИВЕДЕННОМУ ВЫШЕ. ОПЕРатОР тач1Х > вычисляет операцию "Прямой. образ" ограничения отношения /г струюуры Крипке иа множестве состояний этой структуры, заданном характеристической функцией Х ь.
гера- // Виачале Сере» все инсвеогес сссчсянча З х: тгсег К:- Ъ»г Хсь:" т х Зх'ч...,а' Гтагйо...,хек'и..., х'„) л Х Гхс„хл*,...,х'„>) г // течгк 1 Мпяе ГХв» Е Х 1: ' яепмв Хь» ~ется 1 бо- ация мио- Пример 10.11 Рассмотрим пример вычисления состояний структурм Крипке, удовлетворяюших темпоральпой формуле ЕО/, Пусть уже построено миакество состояиий 1//, уловлетворяюшпх формуле / (рис.!0.15). Искомое мио- жветеО 1',1аг/ СтРОИтеа КаК НапбОЛЬШаа ИЕПОДВШКИВЯ тОЧКа ОПЕРатОРа твп/(с) =Я~ /эЕХ(У) — предел после/юшпвльности приблшкенпй Ядтяп/(Я)рткц/ (Я)ртвц/ (8)р....
Гпвеа зр Рис. н из нив. чисзв Рнс. 1915, в-е. Псссрсеннс нанбоиелсй неполавкной точвн операзарв с(2) Д~ г~Е)1(У) (к срямеру 1О.! 1) нмх ломе брасз пзи6 з~~ мтО ть(3) б1 гт ~(В) 1 д юге 1Е 1б г и д, Построение наибольшей нслоленмной точки оператора т(2) = Д~ гч ЕХ(Я) (к примеру 10.! 1) Рнс. 10.15 показывает, что нв кшклом шаге из предваригелыю помеченных состояний оспнотся помеченными только те состояния, которые помечены Г н нз которых за один шаг можно достичь какого. либо помеченного состояния. Сначала помечено асс мнаасство б.
На первом шаге помеченнммн остаются только состояния Ду, потому что ДушЕХ(о)=Дгшб=Ду. Вычисление тяпу~(о) =,тася (Д.) в нашем примере выбрвсышет два помеченных состоания — иь кажаого из них не существует перехола в уже помеченные состояния. Явные алгоритмы маркировки состояний булуг выбрасывать их последовательно, символьные алгоритмы используют представление ВРР характеристических функций, опнсывмошнх соответствующие множества и операцию коньюнкции. Нв третьем шаге вычиаюние тз (И) выбрасывает еще одно состояние нз помеченных: из него за одни пе Гилее 10 являел аблвдн В1 Дг наимен мерв П Алгорг потони неподв слелук кв опе1 которо нне з, из эи реход нельзя попасть в множеспю помеченных ренее состояний. Последующее применение преабрязовяния к множеству уже помеченных состояний нашего примера не выбросит ни одного ранее помеченною состояния; из всех ннх существует переход в какое-нибудь помеченное состояние.
Алгоритм завершен: мы пришли к неподвюкной точке преобразования. Поскольку процедура была начете а пояиого множестве, полученнвя неподвижная точке — наибольшая. Рис. 1м16. Ревела ваюдвямиых точек оператора тка примере 1О.11 Пв риа. 1Одб показана диарвммв Хяссе всех неподвюкных точек этого операторе (множестве звтемненных верюинь В примере 10.11 текил рвзличнык множеств шесть, все они образуют решетку. Одной из непапвнящых точек Рекуро введен~ преобр сивков этой ф вюкно1 удобен таблиц тинная го опе!ичных ! точек мз .зпч шукь ~який и: из члгозльку ! точ- является пустое мноямство !гг — любое состояние этого мншкесша (рх нет) обладает следующим свойспюм: оно принадлежпг подмножеству мншкества Ду и пз него достижимо сосгояние, облажжицее этим же свойством.
Это наименьшая нз неподвижных янек оператора ткцг. Решением задачи примера 10.1 ! авлястсл наибольшая из этих неподвюкных точек. Алгоритмы построения наибольшей н наименьшей неподвижных точек монотонного оператора т на множестве Я дшт теорема Тарского. Остальные неподвижные точки можно построить перебором. Здесь они построены по следующему правилу.
дн«туемому видом оператора т: неподвюкная точка оператора тхцГ (с ) = ДГ ш ЕХ(У) — это любое мнаксство состояний М, котоРое Явлштсл поДмножеством множества !'„Гу, и если в М входит состоЯ- ние з, то нз з есть переход в сосгоянне нз М. Рекурсивное определение всех остальных формул темпоральной логики СТ(„ введенное в разделе 2.3 гл. 2, дает возможность определить искомые мншкества состояний структуры Кринке как неподвюкные точки соотвсгствующнх преобразований. Построим таблицу, в левой части которой запишем рекурсивное определение темпорзльной формулы, а в правой части — определение этой формулы кая наибольшей (тУт(У) ) нли наименьшей ( ИЕт(с) ) неподвижной точки оператора на множесше состояний структуры Кринке. Для удобства будем понимать шждую темпсрвльную формулу в правой чвсги таблицы квк множество таких состояний структуры Кринке, на которых истинна эта формула.
глава Ш 16.10. Закл)очение Алгоритмы промркн модели осуществлюот вычисление множества состояний струкгуры Кришсе, на шпорам выполняется заданная формула темпо- ральной логики. Увеличение числа компонентов верифицируемой системы или увеличение числа переменных экспоненциально увеличиааег число сосгояиий структуры Кринке, явлвющейся моделью сиегемы. Этот эффект, названный "взрывам часяа состояний", ограничивает применение обычных алгоритмов верификации шабе) сйесЫпй. Алгоритмы верификации, работаю. щие с явнмм предспшленнем состояний анализируемой системы и оперирующие состояниами и переходами последовательно, одно эа другим, могут быть нспользованы только для проверки "игрушечных" систен. Разработанные сравнительно недавно "иеяеяые", или "символьные" алгоритмы, которые используют очень эффективный метод лредставленйя дискретных данных — множеств и отношений — в виде булевых функций а форме бянарных решжощих диаграмм (В()В), позволяют увеличить число состояний вернфицируемых систем до астрономических значений.
Для логических схем и программ раюаботины очень эффеативные системы символьной верификации, что привело к возможности использования алюритмов верификации пкя)е) сйесЫлй для реальных, разрабатываемых промышленностью систем и сделало верификацию этапом технологии разработки промышленных систем. Обоснованием алгоритмов проверки свойств, вырюкенных формуяами темпоральной логики СП., лвляетса опредеяенне этих формул с помощью неподвижных точек (наибольших или наименьших) операторов на множестве состояний структуры Кринке. Теорема Тарского даст простые н ясные алгоритмы вычисления наибольших и наименьших неподвижных точек таких операторов. Эти вычисления могут быть реализованы либо явными алгоритмами, рабстыощимн с кшкдым элементом обрабатываемых множеств, либо неявными (символьными) алюритмаыи, работающими с булевыми функциями в форме В()(), представляющими этн множества.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
