2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 83
Текст из файла (страница 83)
При верификации графа регионов используется обмчнмй для СТЬ алгоритм раэметки состояний структуры Кринке теми подформулами проверяемой формулм, которые в этих состояниях вмполияютса. В формулах логики СТ1. в этом случае не используется темпорельнмй оператор Х (МегсТ1те 1 как с квантором существования ЕХ, так и с квюпором всеобщности АХ: в системах с непрерывным временем говорить о "сясдуиа,мн моменте времени" дла систем реального времени бессмысленно. в!э В качестве атомарных предикатов формул СТС прн анавизе систем реального времени можно использовать не только атомарные преднкаты (в том числе имена локапнй), ио также и соотношения между значениями локальных часов временного автомата, структура которых определена грамматикой: ?:жх-с!х-у-с! ?)улу, где с — натуральное число, х, у — локальные часы, а отношение - принадлежит множеству (х,<) .
Таким сбрюом, формулами СП. прн проверке свойств временных автоматов могут быль логические формулы, включающие как атомарные преднкаты, так и ограничмшв на локальные часы. Например, формула СТ?л ЕР(р л (х<3) л(х-у>0)) говорит о том, что в автомате из начального состояния сущссгвует путь, при- водящий в состояние, в котором выполнжтся атомарный предмет у, и при этом показание лоюшьных часов х меньше 3 н больше, чем показание ло. квльных часов у. Рассмотрим несколько примеров. Медля дяя юму зиов знтм :мой СТ1.
сис. енн" Поскольку начальное состояние ?, графа регионов-й(лз) входит в множест- во йн(ф), то формула ЕРАСг выполняется в й(лэ) и. следовательно, вы- полняется во временном автомате лз, Пример 12.9 Проверим, выпслнвется ли во временном автомате Лз рнс. 12.13 свойспю ЕРАСг — существует таксе вычисление, на котором найдется соспжние, нз которого все дальнейшие вычисления будут проходить через состоянив, помеченные г. Формулу АСг пресбрвзуемтак: АСг= Е Сг= Ер г.Погрвфурегнонов й(лз) (см. Рис.
12.13) последовательно находим мышкеево его состоаний, удовлетвориощнх подформулам формулы ф = И Ер г: У! =-' МЛ) =(Рп чз. чз. че) Уз ЕР?з 'йн(уэ) (Ч! Чз Чз Че Чэ Ча Чт Чз Чэ Ч!2 Ч!4) Уз --Уз; й.(Хз) =(Ч!е, Чп, Ч,з) ф=?4 ЕРУз' Йн(ф) =(Чп ..., Чм) Рвала Щ С помощью графа регионов проблема достюкимостн во временном автомате решаетса достаточно просто. Рассмотрим решение этой прсблены на при- мере. значг прил Пример 52.5й Один из вариантов прозокола взаимного исключения Фишера для параллельной программы, состоящей из двух последовательных процессов Р и Рд, формулируется так.
Процессм Р, и Рз взаимодействуют через разделяемую переменную у'. Каждый из процессов независимо устанавливает значение разделяемой переменной соответственно в ! нли 2, а затем входит в свою критическую секцию при условии, что установленное значение разделяемой переменной сохранилось тем, которое было этим процессом установлено: ! раф выем рис. Гзы а,: г:-» ьн ««зе !г-!!я ,: связь а з Рг .'.' вн г:2~ вм ««ае !я-г1г се,: о«а«низ а Почти очевидно, что этот протокол некорректен. При анализе параллельных программ их обычно рассматривают как совокупности асинхронных процессов, абстрагируясь от времени выполнении операций. При такой абстракции этот протокол действительно некорректен. Из параллельной композиции соответствующих структур Кринке можно заключить, что в этом протоколе существуют вычисления, приводящие к состоянию, в котором оба процесса находется в своих цинических секциях.
Одно из таких вычислений: На этом вычислении свойство взаимного исключения нарушается: на нем достижимо некорректное глобальное состояние сл, лслз; оба процесса вошли в свои критические секции. В терминах пюбе! сйесЫпй для этой модели выполняется формула ЕР(сз, лсгз) логики СП.. Проведем более тонкий анализ протокола Фишера. Проверим, достижимо ли некорректное состояние в этой параллельной программе, если временем выполнения операций не пренебрегать, как это делается в асинхронной модели.
Временные автоматы, представляющие этот протокол, пакюаны на рис. 12. ! 5, а. Для учета времени выполнения операций используются локальные часы х и у этих процессов. Отличие от асинхронной модели состоит в том, что временные автоматы, моделируклцие взаимодействующие процессы, учитывают здесь время выполнения операции проверки значения разделяемой переменной У': каждый процесс дшокен установить общую переменную 12 )ь- 2 ~ю зй Рр 1 б ях оси ле са яи и. на ~ь- в Г менее чем через ! единицу времени после старта, а операцию проверкц значения у не может выполнить менее. чем за !единицу времени после прихода вычислений на метку Ь,, Граф регионов Й(Р! !~ Рз '! содержягг около 70 состояний.
Фрагмент, показывающий два возможных вычисления зтого графа, представлен на рис. ! 2 ! 5, е. Анализ показывает, что после входа одного нз процессов в свою Рне. 12.1 $. я) Временные автоматм лля протокола Фншсрв; б! репюны дяя двух локальных часов, С Ся ! Глава Т2 Спсяь н1РДР,1с х рис. 12.! Е в) Фрапчент графа регионов лля протопив Фимера критическую секцию, изменение значения общей переменной у другим процессом невозмохгно. При любом развитии вычислений два процесса не могут находиться в своих критических секциях одновременно. На структуре регионов рис.
12,15, б показаны изменения значений локальных часов этой параалельной программы лда траектории вычисяения графа регионов оггз ... 1п. Монне сделщв вывод. что протокол взанм»ого ис«люче»»я Фищера корректен: глобальное сосюяние, удовлепоряющее формуле ся, лсзз недостюкимо: формула ЕР(сз, нщз) на графе регионов Н(Р, йРз) не выполняется. Пример 12Л1 На рнс. 12.16 приведен временной автомат Ае и его граф регионов Н(Аь) . На структуре регионов рис. 12.16, б поповны изменения значений локальных ~аесеаатсыата Аь На ВЫ ~НСЛЕИНИ К =13Щезоьсзпвегс%24осз Проверим, выполняется ли в автомате Аь свойспю: Е = Е ~Яо21" Ю (Ая ((О с к с1) л (у = 2)))), а именно, в автомате Ае существует такое вычисление, на котором автомат будет находиться в состоянии о2г' до тех пор, пока не придет в состояние, из которого на каждом вычислении доснвкимо состояние, в котором показаннв локальных часов х находятся мсжяуй и 1, а локальные часы у показмваот 2.
уа2;Ь;х: О а не ре ой ов ~н- О 1 х б Рнс. 12!б,е ив. Врененной автомат Аа и нзнсненне его янов на одном из вычисленнй нз Главе 52 Отме нимае время мой а l а г / г l г ег Р г и„ 12Л вет~ г г / г ь < ь Ч ГЗ "ре ли" с оп ь хио; ~ю2 Гз "со лес П "ер ь Рис.
22Зб, е. Граф регионов автомюа !94 По графу репюное Н(Аб) последовательно находим мшякестаа его состоя- ний, удоялетаоряюших подформулам формулы !9; МА) (% Че Ч9 Ч!с Ч1») 'ип(У2)=(ЧЗ Ч19 %1 Ч12) сег( г»)=(Ч!с) слг(Я=(чя Чя %9) дел(55) (Чс.р! % %2 Ч!з Чы Че») 'ип(Ч) =(ЧВ Ч9 %0) Грань ляет ф Начальное состоание Чс нв входит в мномество сосюаннй, помеченных !Р.
Поэтому формула !р не выполняеюя а графе регионов ге(Аб) и„слепень тельно, яо временном автомате ле. где р кальнь в ТСГ1 пъ.и Я =(0<я<1)! Л=(у=2); У» = Я Ге 52! .54 ~ЖЗ Л» =®оХ; о=и(З»е414)! и и <и, < Чь г Ъ Для с! ность долги! вырая колич лорал! мени: Класа иия ня ко лог ную л ра 0 котор! Напри не бол ззз Отметнм, что при проверке свойств, вырткенных в логмке С"П., обычно мрн- нимтаюл во внимание все возможные траекюрии временного автомата, в то время как при проверке выполнимости формул логики ТСП., рассматривае- мой в следующем разделе, анализируются только дивергентные вычисления, 12.1 О. Временная темлоральная логика ветвящегося времени [Т[тлеб СТЦ Для спецификации свойств систем реального времени вюкно иметь вазможность выразить не только обычные темпорвльные свойства, определяюшне доспакимосп состояний, порздок событий в вычислениях или условия, вырткенные через показания локальных часов временного автомата, мо н количественную информацию.
задаюшую временной диапазон ледствия темпоральных операторов. Примеры таких "жестких" требований реального врсмеми: гьз х Ф. лоаа- где р — атомарный предиквт, у — условия, нтклкеннме на значения ла. кавьных часов, а е — временной интервал, е ш Н. Атомарные утвешкления в ТСТ(. включают ме только атомарные предияатм, ио н првдмхпгы, ностра. П "реокаие но любой вопрос наступит не назпсе, чем через, 10 единиц времени" (Ьоипбеб гевропю); П "событие с не мелеет наступить раньше, чем через у единим времени после последнего настутмния события Ь"; П "временной интервал между событюиен а и Ь ттнятяяет от 1 до и, ие включая и ".
Классическая темпоравьная логика не может вырюиш подобные ограничения на вычисления. Длл вырткення таких свойств было предложено несколько логик. Мы рзссмотрни здесь Т(шеб СТС (ТСТЦ вЂ” временную темпораль-. ную логику ветвящегося времени. В ТСТС действие темпоральмого оператора П м выводимых операторов я н С ограничено времеммыми рамками, которые указываются непосредственно у темпорального оператора. Например, требование того, что всегда после посылки запроса ответ придет ме более чем через (О единиц вртоенн, моют выразить так АС(гебиеяг ыь А(гз~сгезроше) Грамматика ТСП, (Т(шеб СТ$,).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
