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

Условиеelse становится выполнимым в операторе выбора, только если ни одно другое условие впроцессе в той же самой точке контроля потоком не выполнимо. Предыдущий примерпреобразуем в эквивалентный следующим образом:active proctype counter(){do:: (count != 0) ->if:: count = count + 122:: count = count - 1fi:: else -> breakod}Условие else становится выполнимым именно тогда, когда !(count != 0) или, что то же(count == 0), и потому сохраняет возможность выхода из цикла.Другим способом завершения цикла является использование безусловного перехода операторgoto.

Оператор goto всегда является выполнимым, если существует метка, на которуювыполняется переход. Это проиллюстрировано в следующем алгоритме Эвклида нахождениянаибольшего общего делителя двух положительных чисел:proctype Euclid(int x,do:: (x > y):: (x < y):: (x == y)od;done: skip}y){-> x = x - y-> y = y - x-> goto doneгде выполнение goto вызовет передачу управления на метку done.

Метка может бытьпоставлена только перед оператором. Здесь метка стоит перед оператором завершенияпрограммы. В этом случае пустой оператор skip является полезным: он выступает какоператор-заполнитель, который всегда является выполнимым, но не производит никакогоэффекта.1.4Некоторые примерыРассмотрим несколько полезных примеров, демонстрирующих возможности языка Promela.Следующий пример определяет фильтр, который получает сообщения из канала ch и делитих на два канала large и small в зависимости от значения полученных данных.

Константа Nопределена как 128 и size определена как 16 в двух макро определениях:#define N128#define size 16chan ch= [size] of { short };chan large = [size] of { short };chan small = [size] of { short };proctype split(){short data;do:: ch ? data ->if:: (data >= N) ->:: (data < N) ->fiod}large ! datasmall ! datainit{run split()}Очевидно, что в данной программе процессы заблокируются в начале работы, т.к. splitбудет ждать сообщений из канал ch, но этот канал пуст! Ни один из процессов не отправляет23в него сообщения.

Введем процесс, который объединяет два потока входных данных в одинвыходной поток, направляемый в канал ch в произвольном порядке:proctype merge(){short data;do::if:: large ? data:: small ? datafi;ch ! dataod}Если модифицировать процесс init следующим образом:init{}ch ! 345; ch ! 12;ch ! 6777; ch!32; ch ! 0;run split();run merge()то разделяющий и объединяющий процессы будут выполняться бесконечно.

Действительно,изначально init отправляет сообщения в канал ch. Далее процессы merge и splitпостоянно поставляют сообщения во входные каналы друг друга. Ни один, ни другойпроцесс не имеет условий, по которым работа может считаться завершенной.Процессы могут быть смоделированы как рекурсивные. Возвращаемое значение передаетсяобратно в вызывающий процесс посредством глобальной переменной или через сообщение.Следующая программа демонстрирует работу рекурсивного процесса.proctype fact(int n; chan p) {chan child = [1] of { int };int result;iffi:: (n <= 1) -> p ! 1:: (n >= 2) -> run fact(n-1, child);child ? result;p ! n*result}init{chan child = [1] of { int };int result;run fact(7, child);child ? result;printf("MSC: result: %d\n", result)}Процесс fact(n,p) рекурсивно вычисляет факториал n, передавая результат с помощьюсообщения своему родительскому процессу p.242 Описание верифицируемых свойств средствами Promela и SPINПодход к верификации на основе метода model checking состоит в том, что для моделисистемы формально проверяется выполнение логической формулы, выражающей некотороесвойство ее “правильного” поведения.

Обычно понятие “правильного поведения” включаетнекоторое множество свойств, которые делают систему полезной для использования, и всеэти свойства должны быть проверены последовательно, одно за другим. Свойствараспределенных систем традиционно разбиваются на следующие классы:••••cвойства достижимости (reachability), которые устанавливают, что некоторыеспецифические состояния системы могут быть достигнуты;cвойства безопасности (safety), устанавливающие, что нечто плохое, нежелательное,никогда не произойдет с системой;cвойства живости (liveness), устанавливающие, что при некоторых условиях нечто“хорошее” в конце концов произойдет при любом развитии процесса;cвойства справедливости (fairness), устанавливающие, что нечто будет выполнятьсянеопределенно часто.Свойства достижимости являются одними из наиболее часто проверяемых классов свойствпараллельных систем: некоторая конкретная ситуация в процессе функционированиясистемы случится.

Свойство достижимости естественным образом выражается LTLформулой EFϕ.Свойство безопасности гарантирует, что при некоторых условиях некоторая ситуацияникогда не может быть достигнута (гарантия того, что нечто плохое никогда не произойдет).Свойство безопасности выражается формулой G¬ϕ. Типичные примеры свойствабезопасности – взаимное исключение, свобода от дедлоков (блокировок), сохранениеинвариантов. Свобода от блокировок является одним из главных требований к параллельнымсистемам: блокировки возникают, когда каждый процесс из группы параллельноработающих процессов ожидает некоторого события (например, каждому процессу дляпродолжения его работы необходим ресурс, уже захваченный другим процессом, и каждыйпроцесс, захватив ресурс, ждет освобождения другого нужного ему ресурса другимпроцессом).Программы, которые ничего не делают, всегда удовлетворяют требованиям безопасности: вних ничего не происходит, поэтому и ничего плохого наступить не может.

Очевидно, чтотребования безопасности в спецификации программ должны сопровождаться требованиямиживости, прогресса вычислений системы в нужном направлении. Прогресс в “правильном”направлении обеспечивается свойствами живости. Свойство живости утверждает, что нечтохорошее в будущем обязательно произойдет, что выражается формулой CTL AFϕ, или нечтохорошее обязательно в будущем будет происходить неопределенно часто, что выражаетсяформулой LTL GFϕ.Во многих случаях выполнение свойств, определяющих корректное функционированиемодели, должно проводиться только на тех вычислениях, на которых выполняется некотороедополнительное условие, которое называется требованием справедливости:fairness ⇒ свойствоСуществует две причины возникновения требования справедливости. Первая причинасостоит в том, что анализируемая система будет работать в некотором окружении, кфункционированию которого мы формулируем эти требования, поскольку только с этимидополнительными требованиями к окружению наша система может выполнять полезнуюфункциональность.

Например, справедливый планировщик должен удовлетворятьтребования предоставления ресурса от каждого процесса. Вторая причина совершенно25другая. Она состоит в том, что в той модели переходов, которая используется приверификации для представления реальных систем, могут существовать нереалистичные,нереализуемые траектории (вычисления), возникшие из-за ограниченных выразительныхсредств модели. Назовем нереалистичные траектории поведения модели несправедливыми.Справедливые траектории поведения системы в этом случае не нужно специальнообеспечивать при реализации: например, реальный канал сам обеспечивает ненулевуювероятность доставки сообщения, но проверку свойств системы нужно выполнять привыполнении условий справедливости – фактически, отбрасывая нереалистичные траекторииповедения модели.При разработке параллельных систем, кроме специфичных требований, которым должноудовлетворять поведение данной конкретной системы, для системы следует проверять еще иобщие свойства, гарантирующие отсутствие некорректностей, типичных для параллельныхсистем.

SPIN поддерживает верификацию следующего набора общих свойств, называемых вSPIN базовыми:• из класса свойств безопасностиo проверка сохранения локальных инвариантов, описанных при помощиоператора assert;o проверка на наличие некорректных конечных состояний, т.е. обнаружениевзаимных блокировок процессов;• из класса свойств живостиo проверка отсутствия бесконечных циклов, не содержащих операторов,помеченных меткой progress;o проверка отсутствия циклов, с бесконечно частым выполением операторов сметкой accept.2.1Оператор assertОператор assert, позволяет задавать локальные инварианты, т.е.

такие свойства, которыедолжны выполняться в определенных точках программыassert(любое выражение Promela)Если выражение, стоящее под оператором assert,истинно, то оператор assert не производитникакого эффекта. Если выражение будет ложно при симуляции, то SPIN выдаст сообщение«Error: assertion violated».

При выполнении базовой верификации свойств безопасностинарушение операторов assert проверяется на всех конечных вычислениях. В SPIN в режимесимуляции могут быть проверены только свойства системы, описанные оператором assert.Все другие механизмы описания свойств, поддерживаемые SPIN, интерпретируются только врежиме верификации.2.2Метка заключительного состояния (end)Когда Promela используется для спецификации модели, которая будет верифицироваться вSpin, пользователь может делать индивидуальные утверждения о поведении, котороемоделируется. Например, если код проверяется на наличие взаимных блокировок,верификатор должен уметь отличать нормальные, с точки зрения пользователя,завершающие (заключительные) состояния от не нормальных.Нормальное заключительное состояние может быть состоянием, когда каждый процессправильно достиг конца тела описания программы, и все каналы сообщений пусты.