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

Рисунок 8. Пример сети Петри. 

Обычный конечный автомат можно рассматривать и как реализующий 
преобразование бесконечных последовательностей стимулов, тогда его принято 
называть 

-автоматом [135]. Обобщенные автоматы также могут иметь 
бесконечные множества состояний, стимулов или реакций, могут использовать 
несколько типов стимулов или реакций и т.п.
Кроме того, все перечисленные выше дополнительные структуры могут 
использоваться 
в 
различных 
комбинациях, 
давая, 
например, 
взаимодействующие бесконечные временные системы переходов или 
расширенные иерархические сети Петри. Так диаграммы состояний в UML 
(Statecharts) [136] представляют собой взаимодействующие расширенные 
иерархические автоматы. 

Примером исполнимых моделей являются также машины абстрактных 
состояний (abstract state machines), введенные Ю. Гуревичем [137,138]. Каждая 
такая машина основана на сигнатуре некоторой универсальной алгебры, т.е. на 
наборе функциональных символов с определенным количеством параметров 
каждый. Состояния такой машины являются алгебрами с этой сигнатурой — 
множествами, в которых каждому функциональному символу сопоставлена 
некоторая операция с таким же, как у этого символа, числом параметров. Все 
возможные переходы описаны одной общей программой, состоящей из 
инструкций переопределения значения одного из функциональных символов на 
1 
0 
c 
p 
2 

---

57 
некотором наборе аргументов, условных инструкций и инструкций 
параллельного выполнения одного и того же набора действий для всех объектов, 
удовлетворяющих некоторому условию. 
3.3.3. Модели промежуточного типа 
Модели промежуточного типа имеют черты как логико-алгебраических, так и 
исполнимых. Стоит отметить, что часть перечисленных выше примеров может быть по 
ряду причин отнесена к обоим этим классам, например, процессные алгебры имеют 
точный исполнимый аналог — системы помеченных переходов, а машины абстрактных 
состояний определяются как некоторое семейство универсальных алгебр. 
Есть, однако, виды моделей, в которых логико-алгебраические и исполнимые 
элементы сочетаются более прямо. Основные их виды следующие. 

Логики Хоара (Hoare logics) [139] являются специфическим видом логик, 
утверждения которых состоят из формул логики некоторого вида и 
программных инструкций. В простейшем виде это тройки {

}P{

}, где P —