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