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