2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 14
Текст из файла (страница 14)
Темпорвльные формулы, истинные в некотором состоянии вычисления,— зто свойства динамического процессе, харакгернэующие будущее поведение системы — вычисление, начинающееся в этом состоянии. Если некоторая темпоральная формула истинне а состоянии эа вычисления, то говорят, что она истинна для всего вычисления, начинжощегося в этом состоянии (рис. 2.9). кд. е~ю и. 1ь- Рис.2.9. Тем лоральные формулы в юждам состоянии характерюуют сеойажа вычисление, начинающегося в этом саспмиин На рис.
2.9 форыула 9() р выполняется иа всем представяенном там вычислении, а формула С г иа нем не выполняется. Формула С г выоалнвеюя на вычислении, начинающемся с х,. Вали темпоральнел формула не выполняется в состоянии, то ее, как н ложный в этом состоянии атомарный предикат, не будем укпьпать в этом состоянии. В качестве атомарных предикатов е реагирующих системах могут использоваться любые угвержаения, принимающие значение "истина" или "ложь" в состояниях системы, например: "леремеллая х лаюлсижельла" (х > О), "очередь эаееоя к ресурсу луома" (9 = О), "паджеерясделле лосьиин сообщения лаяучело" (гейнеж а ке) . Имя состояния, в котором может находитьая дискретная система (например, метка оператора), также может бытыпомарным преднкатом, Атомарный преднкат, принимающий истинное значение, когда модуль М находится в состоянии э, можно записать как 'Мфэ'.
или, если имя модуля очевидно, то 'аэ', или же просто 'э'. Например: свойство "принтер занят (находится а состоянии нли рюкиме занятости)" эапишестя как 'Ргйиегадиюу', а свойство "процесс М находится в авоем критическом интервале" — как 'М(фст(лг' и т. п. Темпаральная логика оквзвиюь очень эффективной в качестве языка спецификации требований к поведению реагирующих анстем, особенно ллв параллельных и рвспредеяеинмх аистам, в которых именно упорядоченность сабы- ии рн эеы), пь ю- ~ в Ге ые ловлю вз ' Пива 2 тий выражает свойства их корртпиого поведешт. Например, требование взаимного исключения параллельных процессов формулнруатса просто: Е (Ксг(пй п ясг(шз) — ' *иикоеда деа процесса.пе будут иаходитьсл в своих критическгм интервалах одиоеремеиио".
Реагирующие системы обычно строятся из нескояьких компонент, взаииодействующих друг с другом, и проверка свойств таких систем весьма важна: как было указано выше, даже если поведение каждой компоненты абсолютно асио, свойства поведения нескольких таких компонент. функционирующих параллельно и взаимодействующих мткду собой, предсказать почти невозможно. Темпоральная логика н метод люде! спесипй используются, а основном, для спецификации свойств н верификации именно реагирующих систем, Свойства, которые интересуют разработчиков таких систем, обычно выражают возможные последовательности событий, возникающие при функционировании систем во времени, например: ножно ли гарантировать, что запрос сервиса никогда не оспшстся без ответа, всегда ли посланные сообщения булуг достаалаться коммуникационным протоколом без пропусков и дублирования в порядке нх посылки, может лн в распределенной системе коммензхь рий на новость прийти раньше, чем нанесть сама, н т.
п. 2.6. Формальное определение ЕТ~ Формаяьиое опредеяение темпоральной логики линейного времени шютоит из определения синтаксиса — правил построения формул логики, и определения семантики, т. е. правил интерпретации этих формул. ив 2б( лыб Формула линейной темпоральной логики (Ыаеаг Ттпрогй (.ойт) (.ТС ° атомарное ушержденне (атомарный предикат) р, и...; ° или формулм (.Т( связанные логическими операторами —,ч; е или формулы (,Т$., связанные темпорапьнымн операторами Х, П. Прошлое в логике ).Т(. не рассматривается. Более формально структура всех возможных правильно построенных формул ЬТ(.
задается грамматикой: литр~-ц~пчд! Хц~ц() р Пр обход вФЧ ) (Т( е ьз) в б ание нмошнх новтем. ыра- циоврос ~ бу- иро(.Т(. ~мул Таким образом, в логике (.Т(, лополнпмпьно к обычной логике вмеказыщний (пропозициональной логике) добавлены только два темпоральных оператора: унарный оператор Х (№лгугме ) и бинарный П (Улг!)). Два булевых оператора — отрицание и днзъюнкцня — образуют базис (днзьюнктивный базис) логики высказываний: через зти операторы могут быть вырмкены любые лругие булевы операторы. Можно счнтать, что все другие логические опсраторм выводимые, они используются для сокращения записи формул: П ипе молва определить, как сокрюценне для ум -р; П )а)зе — как сокращение для лпе: П р! лрз (конъюнкция) — кмг сокращение длв -+ нр! и фД П р! --.ь от (импликация) — как сокращение два р, и от, и т, д.
Пара темпоральных операторов Х и () образует темпоральнмй базис $.Т(л другие темпоравьные операторы можно выразить через ннх. Чаще всего в (;П. используются выводимые операторы Р н С: П Рр можно считать сокращением для игмЩ; П 'Снр можно считать сокращением для Р р. Семмггнка формул !.Т!. определяется на вычислениях. Это значит.
что формулы ПТ!. интерпретируются (приннммот истинное или лажное значение) на бесконечных цепочках состояний, в каждом из которых атомарные предюаты имеют конкретное нстинностное значение —. «пе илн )а)ле. Любая фор. мула р логики (,ТЪ на конкретном вычислении о=лез,лз ... будет либо нг тинной, либо лохоюй. Обозначим о(!) состояние г, вычисления а, а о' — !-й суффикс цепочки о, т.е. о" л,г, !змз...
Тогда з, !=р обозначает утверждение: "В сосиизяиии л, вьииыилемся (исмаила) формула р" т а о )= Нг — утверждение "На емчислглив аеынолилется формула р ". В соответствии с определением 2лд о~ О иа )=р е т. е. формула истинна на вычислении, сели н только если она истинна в на- чальном состоянии зтого вычисление. О Определеиие2.7(семаюнилв льТЦ Истинность формулы р логики ПТ(. на вычислении а лвтгтз ...
(обо. значаетсв а ~ р ) опрцаеляется нндукгиано по структуре формулы тг: Глазе 2 е,ш| и, если атомарный лрсдикат р иствнеи в начальном соспшнин вычисления с; ° с)= »р ос(е»р — если формула»р не выполняется на с - ° си»р,ч фз и о~ ф»»»с(= »рз — если на с выполняется или формула»р», или формуле»рз, ° сНХ»р м с' Н»р — если ф выполняется на вычислении » с =з»зззз -' ° с~=ф»нфз м(зйдб)(оз( фз»»(29:05/<я)»зг)=ф») — аоки когда-то в будущем состоянии вычисления с (включаи наставшее) выполнится формула фз, а до ее выполнения во всех состояниях вычисления с будет выполняться»рп Значение квантора "Ф' на пустом мнолвстве равно лъя, поэтому определение оператора Уш»» явшется "рефлексивным" в том амысле, что неспмщее является частью будущего.
То же относится и к выводимым темпоральным операторам р' и С: О пирр м(З2 20) о~)»р — если найдется такое 2, что ф выполиясгщ на ь зычно»внии с = згтз+ зь»2- „„С (ц220) з»-ф сади»р выполняетая на ваах соспшншш вычисления о. 2.6. Примеры использования формул 1. П Напомним, по для уменьшения числа необходимых скобок при записи формул ЬТЬ часто используют следующее соглашение о приоритетах операций: все темпоральные операторы имеют равный прнарншт, более старший, чем приоритет любой логической операции. Например, формула Ср ~ргХ»р долхош пониматься твс (Ср)»((йг) г»(Хр)) . При необходимости нли в случае сомнений в темпорельной формуле следует расствиспь скобки, чтобы уиазать порядок выполнения операций.
Иногда вместо значков р', С, Х пишутс, Ц н О. В шой потанин формула Ср юйгХя может выглядеть шш ЦРюфгОр, Пример 2.2 Рассмотрим примеры записи некоторых свойств бесконечных вычислений с помощью формул У,Т).. а) С(рюХС уу — р встретится в будуншм не болев одного раш; ви з) х б) Ву л С(р ю ХС-еу) — е встретится в будущем точно одни раз; в) рюшу — на р, наступившем в начальном состоянии, когда-нибудь в будущем будет реакция р; г) С(роьйр) — иа любое встрстмвшееся в вычислении р всегда в бу- дущем будет реакция д ', д) С(разрз)р) — всегла если запрос р будет подан, реысция р на него обязательно будет получена, в до ее получения запрос р не сбросится; е) Рт ю( р) Ср — если событие р наступит, то до его наступление со- бытие р не несгупит. ример временной днаграммм н ее малешьеычнсюнне'.
Пример 2.3 Свойства поведения дискретных логических схем тоже могут быть описаны с помощью формул логики У,Т).. На рис, 2.! О приведена временная диаграм- ма — график значений двух сигналов на выходе электронной схемы, Сссгоя- ния схемы фиксируются в каждом тыгге. Если единичное значение потенциала принять за логическое значение «ме, а низкое — за логическое значение уаме, то этой временной диагрзмме можно сопоставить ее модель — вычисление, в каждом состоянии которого заданы истинностные значения атомарных предикатов р и с.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
