2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 44
Текст из файла (страница 44)
Если управление взаимным исключением строится с помощью семафора, то Реализаглт семафора должна удовлетворять требшшнням справеллнжкти (например, поддерживать Р(РО очередь процессов, желмощих войти в критическую секцию). В то же время АНАЛИЗ системы процессов с критическими секциями должен проводиться В ПРЕДПОЛОЖЕНИИ, что это требование выполняется.
Иными словами, при анализе должны рассматрнмпься талые» справедливые траектории вычислений. Дла системы процессов примера 5.3 ак 5 ограничения справедливости можно определить так: Р ((РЩтЗЦР2~$лЗЦ вЂ” т.е. кшкдый прогнал может входить в свою кригнческую аекцию бесконечное число раз. Прымпр В.й На рнс. 6.5 представлена модель игральной кости: кюкдый результат бросания кости приводит к состоянию, в котором отражено число очков, выпавших в данном акте бросания. В модели вгжмакны нереалистичные траекюрии (последовательности состояний), например такие, в которых бесконечное число раз выпадает только 6. Очевидно, что в реальности могут выполняться только такие трм«торин, в которых каждая грань кости выпадает неопределенно часто, Если мы используем модель играаьной кости как компонент в модели системы параллельных процессов, то при анализе анстемы мы должны ограничиться только реалистичными траекгориямн повеления.
Назовем их "сл)хмедлаеыми". Ограничения справедливости можно в этом случае определить множеством Р (()Ц2ЦЗЦ4Ц5Ц6Ц: на всех вмчнсленнах агэсдав грань должна выпадать неопределенно часто. Это жа можно выразить ).Т1 формулой Ср'!'лСЕ'2'лСР'4'л СЕ'5'лСР'6' Хош это доасльно слабое требование, поскольку оно не совсем отршезег то, что происходит в действительности (в реальности все грани выпадают с одинаковой вероятностью), однако во многих прнлшкеннях его мшкно считать хорошей аппроксимацией вероятностного выбора. Этот пример показывает, что с помощью пошггна справедливости мояшо учесть реальные свойства ср~м, в которой фующнонирует система Приз Рассь тальк нии,: траек образ инкн) прим~ долж~ денна мощь лов н свойс такие лжна юри- юлуьтога ~шью зпра>щих юв с э это гтриссав так: юса.
шнх грин ьное ться едеит в шжием гчае ~иях то, ~дишть вег, ряс 66. Модщыпрвльного кубика попускает нереелвстнчные еычвсаення Пример 6.10 Рассмотрим комппщцню двух параллельных процессов (рис. 6.6). В глобальном состоянии (апра) композиции возможно выполнение операций как первого, так и второго процессов. Вычналение, в кагором выполняегса операция только первого процесса, соответствует зависанию системы а этом состоянии, хотя второй процесс плов выполнить свой переход. Понятно, что такая траектория вычисяений нереальна, ее можно ачнтать несправедливой. Таким образом, нереализуемые траектории поведения в модели системы могут возникнуть из-за семантики ннтерливинга.
Ограничением справедливости в этом примере будет множество гт=Цз1),(6)Ц: и состояние з,, н состояние рал лалжны встречаться в вычиалениях, на которых асущеспшяегся анализ щже. денна системы, бесконечное число раз. Этак пример покюываег, что с помола ю понятия справедливости можно )'честь ограничения модели перека. дов и нх асинхронной композиции. Заметим, что в режиме удоааепюренна свойспа слабой справедливости в верифнюпоре (например, в язмке Зр~п) жф такие нереальные вычисления не будут аналнзнраваяься. Глава 6 Ом Рнг.6.6. Асинхронная композвшм нрощкжж порожаает нерсалнстячнме выМвпмюм Пример 6.11 Рассмстрнм струатуру Крнпке К, представленную на рнс.6.7, н луп к зе(знзз) на К.
В состояннн з~ есзь выбор между переходамн в состояння зз нлн зз, но на пути я возможность перехода нз з~ в зз всегда нгнорнрустся. Интунтнвно траекторня к не является'реалнстлчной в К: еслн на некотором вычнсленнн бесконечнп часто преллагаетса альтернатнвный выбор между двумя вазможностями, каждая нз ннх рано нлл поздно (нлн даже бесконечное число раз) долясна быль выбрана.
Определнм для струкгуры Крнпке К два ограниченна спрааеллнвостн: Р = ((зз), (зз)), которые имеют следующий сммсл: обе альтернатнвы в состоянии з, должны выбнраться неопределенно часто на любом вычнсленнн К. Вычнсленне к не удовлетворяет этим ограннченням справедлнвостн: в нем вовсе не встречается состоянне зг ° Такам обрюом. с помощью ограничения спрзведлнжктн можно лскяючнть те вычнслення моделн, которых в реальной снсгеме нет(еслн вычлслення, на которых одна нз альтернатив бесконечно нгнорнруется в альтернатнвном выборе, считать неревльнымн (неспрзведлнвымл)).
Как най чгс( тнм сем~ бы ~ чнсг тнкс Инн ной Итю мож с до лизе Люб рова СЩЧ Вь Рис, б.т, Струьтзтм Кривее, в коюрой присугствуст аяьтериативныл выбор путь >ует:ото- чежлгже ~уры геют г не- оря:тоячить г, на вы- Квк видно нз зтих примеров, определение ограничений справедливости квк набора подмножеств соеюяннй структуры Кринке весьма удобно.
Однако, как было доказано в И5], зто свойство невыразимо формулами СТЬ. Для того чтобм остаться а рамках СТТ. и использовать разработанный для СТК аффективный алгоритм верификации, в [3 Ц было предложено несколько изменить семантику формул СТО так, чтобм вмполнимость формул СТЬ определялось бы не на всех вычислениях структуры Кринке, а только на справедливых вычислениях. Такая семантика формул СП. нюывастся "стйкнедяаеой" семантикой. Нюке мы рассмотрим, как должны интерпретироваться формулы темпоральной логики аепжщегося времени на справедливой структуре Кринке.
6.7. Справедливая СТ$. ($а! р СТЦ Итак, условия справедливости выразить в логике СТО невозможно. Однако можно изменить семантику формул СТК так, чтобы они интерпретировались с допалинюльиым условием справедлимюти таким образом, чюбы при анализе несправедливые вычисления игнорировались. нв 6.2 "Справедливой" структурой Кринке 54л назовем структуру Кринке с множеством ограничений справедливости: лгг =(Я,бс,Я,АР,Е,Р), где ограничение справедливгюти Р ~ 2' есть мнвкество подмножеств состояний структуры Кринке.
Любая формула СП. в справедливой структуре Кринке доюкна инюрпретироваться ие иа всех возможнмх путях, которые ведут из данного состояния структуры Кринке, а только на справедливых пупы. Заметны, что это условие совпадает с условием допуска м-слов в обобщенном автомате Бюхн (см. гд 4). Прн пустом мнткестве Р справедливая структура Кринке эквивалентна обычной структуре Кринке: в ней любой путь является справедянвым. Определим справедливую семантику длв базнса (ЕХ, ЕП, ЕП~ иогнкн СГ~.. Для структуры Крнпке Мл =(б,бе,)Г.АР,й,р~, где Р (У),УЭ,...,Уь~, обозначим Мг, э )=я Ф следующее угвсрмденне: формула Ф удовлствораегся з состоянии з структуры Кринке Мл прн ограннченнях справедливости Р .
Введем'в рассмотрение новый атомарный прелнкатуай' — ему удовлетворяют все такне состоання справеллнвой струкгуры Кринке Мл, нз которых сутеслм)чт вмчнсленне, проходтцее через состояння кткаого нз мнохгестз У),8Э,...,Уь бесконечное число реэ, Рассмотрнм, как построить мтпкестео состояний, в которых этот атомарный преднкат нстннен. о 8.8 Справедливой ССК (снльно связной компонентой) структуры Крнпке Мл будем называть такую ССК, котврая пересеквеюя со всеми мноществамн У),У2,...,Уя. о утеерждетт $313, лемма 4Л) Преднкатут нстннен и состоянии з ятгда и тамно тогда, когда в структуре Кринке Мл существует достюкнмвя нз э справедливая сильно сапная конлоягнта (рнп б.8).
, Рвг.6.8, Состояния структуры Крыме, в нпосмх нстннсн втомарныя врелнттуаГг В со ° к03 рь кс нс Поме тяо! Гег ь дэЮ) тнкоя С Вь вс 2. Вв 3. Эт, йг Поскс атома~ анй, ) форм) Рч оз тогда со спр Следу~ сзрувт справе гсс гщентдук -Ть. .тся ° ВОДЯ- гх су кеств ество мно- гда в знзая В соотвеютвии с зщм утверждением, определение миакества состояний Ял, ° которых выполняетгл атомарный предикатушг, состоит нз трех шагов! гУ находятся все сильно связные компоненты Мл. Назовем нх ССК!, ССКь ..., ССКВ З находятся спрзведливые снлыю связные компоненты Мя, т. е. те, кото.
рые пересекаются со всеми множестщмн р! ограничений справедливости; З строится множество Ял а 5 состояний Мл — это все такие состояния, нз юторых доспокима хпщ бы одна справедливая сильно вещная компонента. Покатим все состояния нз 8л атомарным предикатомуйгг, используя функ- щно пометок Е: пм езь еез, се ьгз]:- ьгегы! ящг ! Ве алгоритм маркировки состояний Мя в соответствии со сприаедянвойсеещгм тнкой лля каждой подформулы чг формулы Ф выполняет следующие пжгн! !. Вычисляетса мнакество состоаний оггглз;(!д), в которых чг выполняеюв в соответствии со справеллнвой семантикой.
2. Вводится новый атомарный прелнкат рт. 3. Этим атомарным преднкатом помеюпоттл все состоянию нз множества Яггле(ж). Ноакольку обрвбопш кюкдой формулы гд щканчиваеттл ююдением нового атомарного предиката рв н маркировкой этим предикатом р„всех состоя° нй, удовлетворжощнх чг, то на кюкдом шаге алгоритма элементами под.
формул являются атомарные пргликвты. Заметим, что атомарный предикат р„означает выполнение формулы ж, поэтому рт истинно в состоянии з зада и только тогда, когда выполнимость !д в з определена в соответспщн со справедливой семантикой. Следующий азгорнтм вычисляет мншксство мг! ы,(Ф) таких состояний сгруктуры Кринке, в которых формула Ф выполняется в соотвсгсщнн со справеллнвой семантикой в юз о< ' я !е! и яег азу те зсь!е! Вятв !ч'! 1 пе ' игатоЫЧ'): Знеии(Ч'): З„> Еаег„,(Ч'); ( нез, > реЫе) )> Вне и(н/>: ( знз, ( ПеЫн)» ваном(ЧЧ:" ( зез/( р,чеь(н) >> зас (ч'): знс( вх(р га>ю)» Зае (Ч>: аае( П(вп(чнГМ. )) )> спинное Знсг„, (Вер) /* анзнлелено нине */ Р р зч ° хр п(сыр| жгр ° нп нньи>ь /* состоянии ин Звени(Ч') нсамнае» нонны аинм>нны нреникато» рт */ пж ньь зе засим(Ч'> ео ь(з>:-ь(з>ы( р, > е спра исти гори кого Здес> еле к вым; Рассмотрим згот алгоритм.
Алгорн>ы работает )Ф~ раз, выделяя подформулы формулы Ф, начиная с самых виугренних (здесь )Ф~ — число подформул формулы Ф). Основным оператором алгоритма является переключатель ° мсмь котормй обрабатывает различные подформулы Ф так: ЧЬСО>Š— В З На СПРааЕДЛНВЫХ ВЫЧИСЛсинак Мг ВЫПОЛНЯЕтеа атОМаРНЫй предикат етое, если в з истинен атомарный преднката гньг, т.е, если 3 и Яг ,' Чьп — в г на справедлнвык вычисяеииях Мг выпслняеюя атомарный про.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
