Методы верификации программного обеспечения

Рисунок 6. Примеры конечных систем переходов. 
Системы переходов являются исполнимым аналогом алгебр процессов, для 
многих таких алгебр за счет определения подходящих видов стимулов и реакций 
можно каждый процесс представить как систему переходов. 

Другое обобщение конечных автоматов — расширенные конечные автоматы 
(extended finite state machines, EFSM) [127]. В расширенном автомате, помимо 
состояний (которые здесь называются состояниями управления) и переходов 
есть конечное множество внутренних переменных, способных принимать 
различные значения. Полное состояние расширенного автомата, обычно 
называемое его конфигурацией, включает текущее состояние управления и 
текущие значения всех переменных. Стимулы и реакции могут иметь 
параметры. Помимо стимула и реакции, каждый переход помечен также 
охранным условием (условием блокировки, предохранителем, guard condition) и 
действием (action). 
Охранное условие (указывается в квадратных скобках) зависит от переменных и 
параметров стимула и определяет дополнительное условие выполнения данного 
перехода. Т.е. для того, чтобы переход выполнился, мало подать на вход 
автомату нужный стимул, нужно еще использовать такие значения его 
параметров, чтобы охранное условие выполнилось. 
0 
2 
1 
4 
3 
5 
6 
8 
7 
?a 
!x 
?b 
!y 
?a 
!y 
?b 
!y 
?a 
!x 
!x 
?b 
0 
1 
2 
?a 
?b 
!x 
3 
!y 
!x 

---

54 
Рисунок 7. Пример расширенного конечного автомата. 
Действие (указывается перед реакцией) определяет новые значения внутренних 
переменных и значения параметров реакции в зависимости от прежних значений 
переменных и значений параметров стимула. 
На Рис. 7 показан пример расширенного автомата, который распознает 
правильно построенные скобочные конструкции, заканчивающихся точкой. 
Пока скобки расставлены правильно, этот автомат выдает OK, как только 
возникает неправильность, выдается FAIL. 

Взаимодействующие автоматы (communicating finite state machines, CFSM) 
представляют собой набор конечных автоматов, некоторые из которых связаны 
каналами для передачи реакций одного автомата как стимулов для другого. 

Иерархические автоматы (hierarchical state machines) позволяют определять 
переходы из группы состояний (но конечное состояние такого перехода должно 
быть только одно!), таким образом экономя на описании одинаковых переходов. 
Кроме того, в иерархических автоматах могут быть группы параллельных 
состояний — несколько групп состояний, объединяемых в параллельное 
семейство. Конечным состоянием некоторого перехода может быть такое 
семейство. Это означает, что после выполнения такого перехода автомат 
оказывается сразу в нескольких состояниях, по одному из каждой параллельной 
группы, входящей в это семейство, и может совершать несколько переходов 
параллельно, если в рамках этих групп есть переходы по одинаковым стимулам. 

Временные автоматы (timed automata) [128,129] — обычно это расширенные 
автоматы, содержащие дополнительный набор переменных-таймеров, значения 
которых изменяются сами по себе с течением времени. Значения таймеров 
1 
‘(’ / x := 1; OK 
0 
x := 0 
‘.’ / OK 
‘)’ [x > 1] / x := x–1; OK 
‘(’ [x = 1] / x := 0; OK 
2 
‘.’ / FAIL 
‘(’ / x := x+1; OK 
‘)’ / FAIL 

---

55 
можно использовать в условиях переходов, изменении переменных или 
значениях параметров реакций. Кроме этого, таймеры можно запускать в 
действиях, связанных с переходами. Запущенный таймер начинает отсчет 
времени с 0. Время может быть дискретным или непрерывным, что позволяет 
моделировать поведение разнообразных систем реального времени. 

Еще один пример обобщенных автоматов — гибридные автоматы (hybrid 
automata) [130,131], 
применяемые 
для 
моделирования 
систем, 
взаимодействующих с непрерывными физическими процессами. В этих 
автоматах часть переменных обычно имеет значения, изменение которых 
описывается системой дифференциальных уравнений. 

Примером моделей с возможностью явного описания параллелизма являются 
сети Петри (Petri nets) [132-134]. В сети Петри есть состояния и переходы, но 
один переход может связывать два произвольных множества состояний (одно из 
них может быть пустым), соответственно, есть множество начал перехода и 
множество его концов. При изображении сетей Петри состояния показывают 
кружками, а переходы — линиями, «барьерами», которые могут соединяться 
входящими и выходящими стрелками только с состояниями. Кроме этого, есть 
набор меток или маркеров, которые расположены в состояниях сети и в ходе ее 
работы переходят из одних состояний в другие по переходам. Переход 
срабатывает, если в каждом состоянии, из которого он выходит, есть маркер, и 
при его срабатывании по одному маркеру из каждого входного состояния 
пропадает, а в каждом выходном состоянии добавляется по одному маркеру. 
Показанная на Рис. 8 сеть Петри моделирует работу блокирующего буфера, 
способного хранить два элемента. Переход с пустым множеством начал сверху 
представляет активность поставщика, который может попытаться положить что-
то в буфер — при этом в состоянии p возникнет маркер. Аналогичный переход 
снизу представляет активность потребителя, который может попытаться забрать 
объект из буфера — тогда маркер возникает в состоянии c. Состояния 0, 1, 2 
вместе с передвигающимся по ним маркером представляют состояние самого 
буфера, номер состояния с маркером совпадает с количеством объектов, 
лежащих в буфере. 

---

56 
Обобщения сетей Петри могут использовать несколько типов маркеров, 
дополнительную разметку переходов и состояний, кратные переходы и пр.