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