И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin, страница 7

Но это неозначает, что все процессы кода ДОЛЖНЫ достигнуть конца своего тела программы.26Для того, чтобы сделать понятным для верификатора, что такие альтернативныезаключительные состояния допускаются и не являются дедлоком, в модели можноиспользовать метки заключительного состояния.В примере, реализующем взаимно исключающий доступ к ресурсу при помощи семафораДейкстры, добавляя метку, начинающуюся со слова end к оператору цикла#define p#define v01chan sema = [0] of { bit };proctype dijkstra(){byte count = 1;endpoint: do:: (count == 1) ->sema ! p; count = 0:: (count == 0) ->sema ? v; count = 1od}active[3] proctype user(){if:: sema ? p;/* критическая секция */sema ! v;/* некритическая секция */fi}мы сообщаем системе Spin, что не будет ошибкой (блокировкой процесса), если в концевыполняемой последовательности процесс dijkstra не достигнет своей закрывающейсяфигурной скобки, а будет ожидать запроса от каких-либо процессов.

Процессdijkstra()выполняет здесь роль семафора. Семафор гарантирует, что не более одногопользовательского процесса может войти в критическую секцию. Поскольку процесс dijkstraявляется обслуживающим, естественно его определить так, чтобы он не знал числаобращающихся к нему клиентских процессов. Поэтому следует рассматривать остановкупроцесса dijkstra в состоянии, в котором его может запросить клиентский процесс овыполнении последовательности операций р и v над семафором, как корректное состояниезавершения процесса.В модели может быть несколько меток заключительного состояния.2.3Метки активного состояния (progress)Так же, как и метки состояния, в процессе могут быть использованы метки активногосостояния progress.

Этими метками помечают операторы, выполнение которыхжелательно, тем самым усиливая необходимость прогресса в поведении модели. Прибазовой верификации модели в SPIN проверяется, что любой потенциально бесконечныйцикл проходит хотя бы через одну метку progress, и таким образом, удовлетворяетсясвойство живости (liveness). Если же находится контрпример, нарушающий данноесвойство, то SPIN сообщает о существовании непрогрессивного цикла, а следовательно, овозможном голодании процессов.

Добавим метку активного состояния к процессу dijkstra,моделирующему работу семафора посредством канала sema. Операции Р и V над семафоромдолжны выполняться здесь внешними процессами, как sema ? p и sema ! v:27proctype dijkstra(){byte count = 1;endpoint :do:: (count == 1) ->progress: sema ! p; count = 0:: (count == 0) ->sema ? v; count = 1od}Считая прогрессом постоянную восстребованность семафора внешними процессами,пометим удачную передачу токена семафором меткой progress, тогда при базовойверификации SPIN проверит, что в любом бесконечном вычислении семафор будетзаблокирован бесконечное число раз.В процессе допускается использование нескольких меток активного состояния.2.4Метка принимающего состояния (accept)Метки принимающих состояний используются обычно в особом процессе never (см.

2.5),хотя PROMELA не ограничивает их использование. Меткой принимающего состояниясчитается любая метка, начинающаяся префиксом accept:accept[a-zA-Z0-9_]*: операторыКаждая метка принимающего состояния в теле одного процесса должна имеет своесобственное имя, например, accept, acceptance, accepting.Фактически, эти метки помечают состояния, которые соответствуют принимающим(допускающим) состояниям автомата Бюхи, описывающим все бесконечные “ошибочные”,“нежелательные” траектории проверяемой программы. Ошибочные траекториихарактеризуются именно тем, что такое принимающее состояние при вычислениипроходится бесконечное число раз.

Поэтому при верификации проверяется, что в системе несуществует вычислений, которые проходят через операторы, помеченные accept,бесконечно часто.2.5Особый процесс neverМногие из свойств могут быть проверены введением операторов assert, меток конечного иактивного состояния в тело типа процесса proctype. Однако, достаточно трудно определитьв модели свойства, подобные данному: "любое состояние системы, в котором p истинно,приведет к такому состоянию системы, что истинно q".

Проблема состоит в том, чторассматриваемые ранее способы описания свойств плохо предназначены для проверки вовсех состояниях системы. Тем более что мы не можем делать никаких предположений оботносительных скоростях процессов, т.е. между любыми двумя операторами процесса могутвыполниться несколько (неопределенное число) шагов других процессов.Особый процесс never дает возможность задания глобальных инвариантов. Процесс neverиспользуется для того, чтобы описать такое поведение, которое НЕ ДОЛЖНО произойти всистеме.

Процесс never предназначен лишь для слежения за поведением системы, неоказывая никакого влияния на нее. В этом процессе нельзя объявить переменные илиманипулировать каналами сообщений. В нем запрещены всякие действия, способныеизменить состояние системы. В модели может быть только один процесс never.Процесс never учитывается только при верификации. Он позволяет проверить свойствосистемы в точности в начальном состоянии и после каждого шага вычисления (т.е.

после28выполнения каждого оператора, независимо от того, к какому процессу этот операторотносится).Простейший вариант использования процесса never – проверка выполнения условия p накаждом шаге системы:never {}do:: !p -> break:: elseodПроцесс never с заданным правилом выполняется НА КАЖДОМ шаге системы. Как толькоусловие р станет ложным, процесс never выходит из цикла и прерывается, переходя взавершающее состояние. Завершение процесса never интерпретируется как ошибочноеповедение анализируемой системы. Если p остается истинным, то процесс never остается вцикле, он не завершается, и ошибки в анализируемой системе нет.Для приведенного свойства можно сформулировать альтернативное описание без процессаnever.

Добавим процесс monitor:active proctype monitor(){atomic { !p -> assert(false) }}Здесь процесс с именем monitor может инициировать выполнение последовательностиоператоров, определенных внутри группы atomic, в любой точке вычисления системы.Поэтому в любом достижимом состоянии системы, в котором инвариант (в данном случаеистинность утверждения р) нарушается, процесс monitor выполняет проверку и сообщает обошибке с помощью оператора assert, т.е. в этом случае процесс monitor решает задачипроцесса never.

Однако, для более сложных темпоральных свойств без процесса never необойтись.Например, рассмотрим свойство:Всегда, если p стало истинным, то когда-нибудь в будущем станет истинным q, а р будетоставаться истинным до тех пор, пока q не станет инстинным.Это свойство достаточно просто описывается формулой линейной темпоральной логики(LTL): G(p → (p U q)) (учтите, что будущее включает настоящее).Рис.

Примеры ошибочных вычислений для LTL формулы G(p → (p U q)). Именно такиетрассы и будет искать процесс never.При проверке модели нас не интересуют все те вычисления, в которых свойствоудовлетворяется, наоборот, для модели проверяется наличие в ней вычислений, на которыхсвойство нарушается. Все такие “ошибочные” вычисления для нашего случая удовлетворяют29формуле !G(p → (p U q)). При верификации нам нужно выявить среди всех возможныхвычислений проверяемой системы хотя бы одно ошибочное вычисление, т.е. такое, вкотором p стало истинным, а q осталось ложным на всем вычислении, или p стало ложнымдо того как, q стало истинным.Очевидно, что нарушение свойства, где q остается ложным всегда, может случиться толькона бесконечных вычислениях. Promela имеет дело с моделями с конечным числом состояний,поэтому бесконечное вычисление появляется только внутри циклов.

Мы не можемиспользовать обычные процессы с assert для обнаружения таких ошибок живости(напомним, assert проверяются только на конечных вычислениях). Воспользуемсяпроцессом never для правильной проверки заданного свойства.never { /*S0:dood;accept:do!G (p → (p U q))*/:: p && !q -> break:: true:: p && !q:: !(p || q) -> breakod}В режиме верификации сначала (в начальном состоянии системы) проверяется возможностьвыполнения первого оператора процесса never. В данном примере выполнение процессаnever начинается с метки S0, которая помечает цикл с недетерминированным выбором.Второе условие состоит из одного оператора с выражением true. Очевидно, что эта опциявсегда выполнима и не оказывает никакого эффекта на вычисления.

Она возвращает процессnever в его начальное состояние. Очевидно, что процесс не может заблокироваться всостоянии S0, т.к. выражение true всегда выполнимо. Наличие true позволяет системе невыполнять проверку свойства, отложив ее на потом.Первое условие первого цикла do выполнимо, только когда выражение p истинно, авыражение q ложно. Этот случай обнаруживает следующее поведение модели: сталоистинно p, но q еще не истинно. Именно с этого состояния может начаться некорректнаятраектория выполнения анализируемой программы.