2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 18
Текст из файла (страница 18)
2.12. Моде! спесЫпя Могзе) сйесалй — зто совокупность моделей, приемов и алгоритмов, позволжощих проверить, что формула темпоральной логики (СТЕь, СП. или ЕТЦ, вырюкаюшая некоторое свойство поведешш динамической системы во времени, выполняется (является истинной) иа модели системы с конечным числом актояний (структуре Кринке). ~в 2 эа последние десятнлппш структуры Кринке епшн общепризнанной моделью реагирующих систем, с помощью которой мшкно адекватно представить поведение реагирующих систем: дискретнмх систем управления, параллельных и распределенных алгоритмов, протоколов и т. п., а темпоральные логики признаны очень эффективным формализмом для выршкения свойств таких систем.
Стандартными шагами доказательства того, что поведение реагирующей системы облвдмт некоторым свойством, являются следующие; К Для верифицируемой системы строится адекватнал модель Крипке л(, т. е. система переходов с конечным числом состояний. Поведения реальной системы представлмотся разверткой (деревом вычислений) построенной струхтурм Кринке. 2. С помощью переменных и параметров верифицируемой системы выражаются интересующие разработчика атомарные предикаты струюуры Кринке — логические выражения, которые могут принимать значения "истина" или "ложь" в кшкдом состоянии системы.
3. Проверяемое свойство выршкается формулой 9 темпоральной лопшн с использованием атомарных упюржденнй, темпоральных операторов н кванторов пути. 4. Проаеряетсл истинность утверждения Дт (= 9 (т. е. угверяаення, что структура Кринке является моделью формулы <р) с помощью полностью автоматизированной процедуры. Метод верификации, реаяизуюший зги шаги, и называется шшЫ сдесдгик. лз )'г. ушего льных м, что го по~учаях к про- траис- Есте- ошло- ьто в Тепле дылу- еннем у поэр вы- 2.13. Заключение ятель- ности о лля юлин- эозво- $.ТЦ, э зрея чис- Задачей временной логики являеюя построение формализованных языков, шккобных.сделшь рассуждения о предметах и явяениах, развивающихся во времени, более ясными н точными, н потому более удобными дая формального анаанза. Темпоральные логики позволяют формулировать угверящения о порядке наступления событий во времени без явного указания времени.
Наиболее удобными зтн логики оказались в применении к спецификации свойств параллельимх программ, в которых важны именно порядки событий, а не явные значения времени наступления этих событий. Л. Лампорт даже определяет темпоральную логику как "формальную систему для спецификации свойств и доказательства их выполнения в пврашмльных программах на всех уровнях их абстрактною описания" [94).
Существует несколько аариапюв темпоральных логик. В области верификации технических систем исполиуются, в ошювном, две такие логики — ло- Гжмв г гика линейного времени 1П. и логика ютившегося времени СТ1.. Обе логики интерпретирувпая на структуре Кринке — недегерминированной конечной аистеме переходов, удобной для прелставвения динамики поведений дискретных систем, Логика линейного времени рассматривает все вычисления структуры Кринке как множеспю беаконечных траекторий поведения системы (граса).
Формулы втой логики построены из атомарнмх утверждений, сшзанных логическими операциами и темпоральными операторамн. Логика ветвящегося времени рассматривает возможные варианты развития вычислений в каждом состоянии бесконечных траекторий. Развитие этих двух типов тем поральных логик частично объясняется существованием двух разных школ, кткдая из которых развивала свою версию темпоральной логики.
Меящу этими школмчн существовало даже некоторое соперничеспю (ам например, название статьи [40]: "Модсмьмости дла тоде! с)мсЬлй: логика еелмящегося еремемн наносит ответный удар"). До с их пор астаеюя открытым вопрос о том, вякая из логик более удобна и выразительна для спецификации свойств реагирующих систем. Обе логики могут быть использованы лля формулировки утверждений о поведении технических систем.
Существуют свойства смогем, выразнмьм в одной логике и невыразимые в другой. Достаточно широко распространено мнение, что свойства систем легче вырткать в логике 1.Т1„в то время как алгоритмы верификщин проще для формул, вырюкениых в СТ(, [! 40]. 2Л4. Замечания Первые попытки учесть раль временного фшпора в логических утверждениях опюсатая еще кантичности.
Идеа введения временных понятий в логику восходит к греческому философу О!адате Сптвз, который жил в!У веке до нашей зры и был современником Аристотеля. Сам Аристотель писал, что конкретное значение истинности высказываний не является раз и навсегда заданным, а зависит ат ситуации, в которой зти высказывания делаютая.
Но талька в 60-х годах прошлого века английским логиком Артуром Прайором (Агбшг Ргюг) была впервые выполнена формвлизвция темпоральной логики, которая была нм названа Тепзе (ой(с [!28], [!84]. Во временной логике А. Прайора были впервые введены темлорааьные операторы Р и Р. Зти операторы (и выводимые из иих операторы С и Н ) вошли в так называемую М!л!пт! Тевзе $.ой!с, которая впоследствии была расширена во многих направлениях.
Различные расширения Тепзе Еой!с изучаются и в наше время. В лингвистике одну пз первых попыток формального анаяиза предложений, ссылающихся на время, сделал Ганс Райхенбах, аовременник Эйнцпейна и Макса Планка. Он писал научные работм по квантовой механике, о природе времени, по вероятности, логике и философии науки. Его идея о возмшкности Ис~ рн4 Раг !мл зиз дяв рал рез том кяа апл сво )тя гра Фо[ Кг! уни еле. та 1 [30' н у най 2.1, соб лол гики »ной дисения юте- свя- ветзний шст- теы3 союдг1 пор льна , ио- сип~мые стем юще чиях гику ;е до что егда . Но )ром нки, Эти мую .
ная. ний, на н !юдс формалюации времен английских глаголов с помощью соотношения моментов наступления трех аобытий 5, Е и Е была высказана в его книге [130]. Использование темпорапьной логики для целей спецификации свойств и ве-. рификации технических систем связано с именем Амира Пнузли (Ащп Рвией), профессора Егтгшапп 1пмипге о( Есапсе, Израиль. до него темпоральные логики использовались только в лингвистике и философии лдя анализа высказываний и рассуждений естественного язь!ка о собьпнях, происхолтцих во времени.
В 70-х голах прошлого века А. Пиузли разработал темпоральную логику линейного времени ([йпеаг Тешрош! (ой!с, [125]) как развитие логики Артура Прайора для спецификации параллельных вычислительных аистем. С тех пор темпоральные логики стали основным инструментом вырюкения свойств таких систем. А. Пнузли также выделил в отдельный класс "реагирующие системы" (гсасизг зузгетз) как особые программные н аппаратные системы, для которых необходимы свои формальные модели и свои особые методы анализа. В 1996 г. Амир Пнуэлн был награжден Тьюрингоаской премией АСМ "за ословопояагающую работу, которая ввела тглиюрагьлую логику е информатику, и за еыдтощийсл вклад е верификацию щю.
грани и систем". Формальная молель "струюпура Кринке" введена в [90] Саулом Кринке (Еап! Клрйс), американским философом и логиком, профессором Принстонского университета. Темпаральная логика ветвящегося времени была введена и исследована Эдмундом Кларком (Едшппд М. С!м]ге), профессором университета Карнеги-Меллон, и Алленом Эмерсоном (Е. Айеп Ешсшоп) в работах [31], [30] и многих других. Полная темпоральная логика СП.» введена Эмерсоном п Халперном в 1986 г.
Сравнение различных темпоральных логик моюю найти а [48]. 2.15. Задачи к главе 2 2.1. Постройте в модели Г. Райхенбаха соотношение моментов насгушнвшя событий Е, й и Е лля следующих предлшкеннй ангянйского языка н расположите зтн события на временной оои: а) Рйшр(е Ргезепц 1 зев 1ойж 6) Раз! Рег(есг: 1 йод зггп уойп; в) 8!шр!е Рпцне: 1зйаИ зев уойн) г) Рюше Рег(еск 1зйаИ йоге зсгл 1айл. 3.2. Пусть р означает "ЯлюблюМашу", а 9 — "ЯлюбюоДшиу". Каким вы- саззываниям соответствуют следующие форьчулы 1 Т[;.
Глеев 2 ге а) р(рю-ьд) б) РПСд 23. Представьте в виде формулы 1,?Ъ высказывание: "Канал может терять сообщение только конечное число рю"; 2.4. Постройте 1.П форыулу, которая будет задавать вычисления со следующими свойствамн: в) если произойдет р, то ? некогда не саучнюя1 б) если произойдет р, то когла-нибудь в будущем выполнится д, а сразу после зтого произойдет г; в) если произойдет р, то затем произойдет д, но менку ними ие произойдет г; г) предикаты р и д выполнмоюя попеременно (т.
е. после р ие встретюсл р, пока не встретится д ); д) если свойспю р, становится истинным после того, как было ложным, то оно будет истинным'точно 2 шага. 2,6. Переведите формулу (РУд) в отрицательную нормальную форму, т, е. в форму, в которой отрицаниа стоят только непосредственно у литералов.
2.6. Какие из следующих формуя являются СП форыуламн? Какие из ннх 1.2Ч формулы? 1. Рч 1 2. АР(р гАСХ д) 3. А(РП(АХд)) 'ь А КС))йг(РПд) 5. Вр(ро АСд) 6. А(рчХднХХ(РП 7)) 2 7. Известно, чго если в формуле Ф ПП. каждый темпоральный оператор будет предварен квантором пугн А, то такал формула СП. не всегда будет эквивалентна исходной формуле Ф .
а) Проверьте, выполняются ли ЬТ1 формула РСр и СП формула АРАС р на структуре Краша М1 (о,бе,й;Ар,б), гле: т лсевгщ вв еа2 (зс г~ зз) 4~=(зс) Ен((вз а>) (зе з~) (зг Ъ) (гз зз)) лР=(Р) ° Фо)йй(~)=(Р) й(з,) =Э. б) Проверьте, выпщщжотся лн ИЧ 4юрмула СЕР н С'П формула АСЕРР на структуре Кринке М2 =(о,йс,й:зР й), где: (зс зг) чс=(зо) ° й=((зс зс) (зе зв) (зпзв)) АР=(Р) г(зе)=йГ 2( )"(Р) 2.8. Можно лн выримть любую формулу СП.ь с помощью операторов ч, Х, 6, Е7 Если да, то вмразнть с нх помощью формулу АР(р =э Х(чбг)) . Постройте структуру Кринке, на которой зча формула вы- .е. нх )р га Рае.2.11.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
