2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 45
Текст из файла (страница 45)
дикат р, если з и Яг, и, кроме того, а з истинен атомарный предикат р; ч( л — в з на справедливых вычислениях Мг выиолняетсз формула р, если з и 8„, а преднкат р ложен в з; т-р ч — в з на справеданвых вычислениях Мг вькюлнвегся формула рой,если зеКг,ив з выполняютсз как р,таки и> Ч/- вв — в з на справедливых вычислениах Мг выполняется формула ЕХр, если из з существует переход в такое состояние, из которого существует справедливое вычисление (т. е.
в нем истинен предикат /и!г ) и а кото. ром истннен атомарный преднкат р. Зту задачу решит нахождение обычным алгоритмом воде! сисой(пй для Ст( формул (с обычной СТ1 семантикой) такого множества состояний, в котором истинна формула ЕХ(рл,/а!г). Здесь используется очевидное соображение: вычисление, которое в>еле первого шага становится спрваедннвым, само будет спрамдливым; хож ( лнкю пс фс ду (З нк На 0 нв яс( Сн (З фо) Рнс. б улове> тн кой. Прим Снова саойсг е буду глава е юмулы )ормул нмттль зарный :.
если ~а р, ормула ормула ушесгв кото ~ычныи зги койз к гл)г). сю пс(В- м - а(впч) — в з на справелливых вычислениях структуры Кринке Мк выполняется формула Е(р()р), если из з существует конечный пусь, асс состояния которого помечены р, в такое состояние. нз которого'существует справедяиаое вычисление (т. е. в нем истннен предииат,~~!г) и в котором истинен атомарный предикат л.
Эту задачу решит нахождение обычным алгоритмом люде! сйьсрбпй для СТ( формул (с обычной СТ( семантикой) такого множества состояний, в котором истинна формула Е(р()(улла(г)). Здесь также используется очевидное соображение: вмчнсаение, которое после конечного числа шагов становится справедливым, само будет справедливым; ч- вор — зта подформула обрабатыммтся специальнмм алгоритмом. Он похож на алгорппн нвхолшения состояний, удовлстворяюшик атонпрному предикату га(г, и состоит из четырех шагов: 0 справедливая модель Мг (т, е, модель, в кюкдом состоянии которой выполняется предикат Уаы ), о~раиичивветая такой моделью мг„, в каждом состоянии которой выполняется еше и атомарный предихат р (напомним, что если р рг для некоторой формулы ж, то ао всех этих состояниях формула у выполняется справедливо, поскольку мы проводим анализ индукцней по подформулам формулы Ф); 0 находатся все сильно свиные компонентм на мпакестве состояний Мя .
Назовем их ССКь ССКь -, ССК ' 0 находятся все справедливые ССК, т.е. тв, которые пересеюпотся со всеми множестаамн У(,...,йз ограначений справедливости. Неэовем нх Снс,...,С,; 0 формула Ебр справедливо выполняема в состоянии з жогда и малько могдо, когда в Мгр из з достижимо хотя бы одно из множеств С,. Рис.6.9 показывает последовательность построения множества состояний, уловлепюряюших формуле Ебр в соашетстюш со справедамаой семантикой. Пример 6.1л Снова рассмотрим струкгуру Кринке Х на рис. 6.7. Проверим наличие у К свойства, выраженного формулой Ф = М'р — нп любых л)пмх когда-набухав е будуцжн есжреллансл и ., Гласе Е Рис.
4.9. С<ктояиня, в ютсрмх формула ййр вмполиются спрзиелянво Дгм проверки преобразуем зту формулу к базису (ЕХ, ЕЮ, Еб) . Поскольку Ар= Е ~р, ЗПР=-,П гр, то Арр ЕС у. Подформулы этой формулы таковьп,У! Р,,У2 - Г1, УЗ=ЮСУ2, Уе--гУЗ, Проверим выполнение свойства Ф Е6 о на структуре Кринке К прн обычной семангмке СП.. Строим множества состояний, на которых выпоанякноя подформулы формулы Ф: 1,г! 4!Яи(11) (зз) — новым атома!зла!и прели«атом У! помемюм состояние зз. 2. у'2 = т!3; оог(у'2) = (дг,зг,яз) — новым атомарным предикатом г"2 помечаем зе,гг зз.
3. г3 =Ейг'2; Строим ССК множества (зе,з!,зз) тех состояний, в которых у'2 выпааияегоя. Эта единственюья ССК (янез) доспщома из всех состояний К, т. е. Йи(уЗ) м(зе,г„гз,зз) . 4. Ф=-!АЗ;йи(Ф)=И. Вывспь в К нет состояний, в которых выполняется формула Ф = АРе . Действительно, в К существует вычисление'я зс(я!,зз), которое никогда ие проходит через состояние Юз. Проверим теперь выполнение свойства Ф= ЕС 4 при справедливой семантике.
В примере б.б определены даа ограничения справедливости: Е =((~),(зз)) . которые имеют сяелующий смысл; обе альтернативы в состоянии з, должны выбираться неопрелеленно чвсю в яюбой траекюрин функционирования к. Дяп справедливой с!Рукгургефрипке кл будам рас- сматр часто Введг котор стоян тольн гся с всех с стоян~ Прове подфс 1. У! 2. у"2 3. уз 4. Ф= Вывод иом о~ нуги и чально ограни пробле ~с ) альку ~мулы при мпал- поме- орых Дсй- ла ие в со. арии ~ рас- сматривать только аправедливме пути, т. е. те пути, на которых бесконечю часто встречаются состоання зз и.зз.
Введем новый атомарный предикат влаги им помеппз состояния К, нэ которых сушествукзт справедлнвме луги. Для того чтобы найти такие соатоянив, посзронм вае ССК мвхкестаа состояний (зе,з„зз,зз». Супнат»уат только одна ССК этого множества С =(зпзз,зз». Множество С пересекатся с каящым иэ Ограничений справедливости — множествамн Р; =(зт» и зз = (зз) . поэтому с — апрвведливал сск. сосгояниа из с достижимы иэ всех мжпжннй азрукьуры Кргщю К поэгому бя = о = (зс 01 02 зз» стояния ю Яз наметим атомарным предиаатом тазг: бзи(»огг) =(зс,зпзз,зз» . Проверяем выполнение свойства Ф= КП с на структуре Кринке Кя по лодформулам Ф: 2 32=ФК А (Г )=(зэ».
2. У'2 -РТ;йп,зь(У'2) (Дг,зпзз» . 3. у'3 =епу'2. для нахождения Язг~ (~3) выполним следукицю ° СПРВВЕДЛИВЗ~Ю Молева КЗ ОГР»нитиааан ДО Модсяк Кгут, ВО Ваек ас аговнззвхкотзгйойаыполюатав 22'бз/2 (зс з! зз» ° стРоим все сск множества (зсзпзз». Зто единствениивсскг (20ьзэ)с ° находим справедливые ССК, т.
е. такие, жпорые пересекаются с ограничениями справедливости Л = (зз» н К2 = (зз) . Таких ССК нет; ° множество соапжний Кз, иэ которых достижимы справейлнвые ССК, пусто, поэтому йзг, (33) И. 4. Ф=-р3; йзг(Ф)=(зс зг 02 02». Вывол: во всех состоанивх Кз фоРмУла Ф = АСО выполиастса пРи ввеДЕниом ограничении справадлимкти (мы рассматривали только аирзмедлиеые пути ю начального состояния).
Поскольку вщ формула еыполиаегся в начальном соагоании Кз, она аыполнаегсв в Кг. Заметим, что опРеделение ограничения справелинжмти только одним мнакеством (зз,зз» не решает проблемы: формула АРО в такой структуре Кринке не выполвмтаж 9.8. Заключение Вюкность выделения классов свойств звюпочвегся в том, что кроме проверки специфических свойств системы важно проверить глюке, что в системе отсутствуют ошибки, типичные для параллельных систем. Если реягируююя система состоит из нескольких взвимодействукицих компонентов, то в ией памзно проверить такие свойстве, квк отсутствие блокнровок, прогресс вычислений ее компонент и т. п.
Неформвльно говоря, свойспш безопвсносги вырвжжпг, что ничего пвохого ие случится, свойства живости — что нечто "хорошее" случится, в свойство спрвщщливости — »то при верификации рвссмвтриввютсв только те вычисления, которые реализуемы в реельной системе. Нвпример, пусть мм строим врбвпр общей шины, которая рвэделяется несколькими процессорвми. Свойство безопвсности в слецификвции арбитра будет состоязь в том, что в каждый момент не более одного процессора будет иметь доступ к шине.
Свойство живости будет вырезать то, что арбитр неопрелеленно часто будет нвходиться в состоянии рвзрешеиия испсльзоввиия шины каким-нибудь процессором, Свойство спрввелливости врбитрв будет вырвжвть, что кюкдый процессор будет иметь доогуп к шине бесконечно часто, в частности, он может захвшизь шину нв произвольное, но конечное время. Метод учета сгрвничений спрелеллимкти состоит в том.
что мы остаемся в рвмквх той же модели — структуры Кринке, но вводим огрвниченне; те вычисления, которые явлжотся ревлнстичными, нвзовем "спрвведли ными" ((е) г), и пытвемся при внвшпе рвссмвтриввть только их. Это ДОПОЛНИТЕЛЬНОЕ требоввние к тем свойстввм, ксторме следует проверять в дискретных системвх. Вычисление будет внвлизиронпъсв нв предмет выполнения требований спецнфнквции, только если нв вычислении выполняется это свойство. Условие спрвведливости чмце всего вводится дяя того, чтобы иметь возможносп отбросить неревлистичнме поведения, явяжощиеся результатом использоввния упрощенной ьюдели.
М<икно считать, что спрвведливвя структура Крипке — зто обычнее струюурв Кринке. дополненнея прмгилом допуске м -слов обобщенного автомата Бюхн. 6.9. Замечания Множество примеров слецификвцни свойств дискретных систем формулвии темпорввьной логики и клвссифшация их в швблоны (рвцещз) дано в (4)). В разделеб.1 испольювяны рсзультвты этой ряботы. Выделение типов свойств (свойств беэопвгмости и свойств жнвмтм) было впервые предложено в (92); впоследствии эти клвссы свойств многократно обсукдпчись, Весьма подробно проблемы спецификации свойств ревгирующих систем и класси- ф» удг жи ии~ рю фо) ел~ Ме цич щи~ спе~ Поз эоп в (т' н м~ ()оз 6.Е ских в) б) в) щ! нв 6.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
