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

3.3.2. Исполнимые модели 
Исполнимые модели (или операционные, executable models) характеризуются 
тем, что их можно каким-то образом выполнить, чтобы проследить изменение свойств 
моделируемого ПО. Каждая исполнимая модель является, по сути, программой для 
некоторой достаточно строго определенной виртуальной машины. 
Зачем моделировать свойства одних программ через свойства других? Для этого 
есть, по крайней мере, три причины. 

В модели обычно учитываются не все свойства моделируемого ПО, а только 
важные для рассматриваемой в данный момент задачи. Поэтому модели 
оказываются значительно проще моделируемых систем, их гораздо удобнее 
анализировать. 

Виртуальные машины используемых на практике языков программирования 
очень сложны и определены нечетко, а виртуальные машины моделей 
значительно более просты и обозримы. Это позволяет провести исчерпывающий 
анализ возможного поведения модели, выявить все классы возможных при ее 
работе ситуаций. 

За счет иного, «перпендикулярного» взгляда на систему часто можно увидеть 
такие ее характеристики и особенности, на которые ранее просто не обращали 
внимания. 
Все виды исполнимых моделей можно считать расширением и обобщением 
конечных автоматов, поэтому их стоит рассмотреть в качестве первого примера. 

Конечный автомат (finite state machine, FSM) [124,125] представляет собой 
систему с конечным множеством состояний, среди которых выделено начальное 
состояние, и конечными множествами воспринимаемых извне стимулов 
(входных символов) и создаваемых реакций (выходных символов). Кроме этого, 
в конечном автомате определен некоторый набор переходов между 
состояниями, каждый переход помечен вызывающим его стимулом и 
выдаваемой реакцией. 
Пример конечного автомата с множеством состояний {0,1,2}, множеством 
стимулов {a,b} и множеством реакций {x,y} изображен на Рис. 5. 

---

52