Верификация автоматов Stateflow

Stateflow - это составная часть Simulink(который входит в математический пакет Matlab), которая позволяет создавать системы автоматов и включать их в состав моделей Simulink. Примеры автоматов Stateflowприведены в разделе 3.8 на рисунке 3.8.1 и 3.8.2.

Верификация автоматов Stateflowсостоит из двух шагов. На первом из них по этим автоматам строится система иерархических управляющих автоматов, описанных в разделах 3.1.1 - 3.1.3. На втором шаге проводится верификация построенной системы.

Первый шаг. Алгоритм построения системы иерархических управляющих автоматов следующий:

1. Автоматы, содержащие параллельные состояния, декомпозируются на систему параллельных автоматов;

2. Для каждого автомата Stateflowстроится автомат :

3. Состояния автоматы Stateflowпереводятся в множество S. Начальное состояние переводится в s₀.

4. Конечные состояния переводятся в множество T.

5. События из автоматов Stateflowпереводятся в множество E.

6. Переменные из автоматов Stateflowпереводятся в множество X.

7. Выходные воздействия из автоматов Stateflowпереводятся в множество Z.

8. Условия на переходах автоматов Stateflowпереводятся в множество B.

9. По переходам автоматов Stateflowстроится отношение δ.

10. По выходным воздействиям на переходах и в состояниях Stateflow строится отношение λ

Второй шаг состоит в том, что построенная система верифицируется методом, изложенным в разделе 3.2.

3.5.