Выводы по главе 3

1. Построены математические модели управляющего автомата, системы вложенных автоматов и системы параллельно работающих автоматов.

2. Изложены предлагаемые алгоритмы построения Spin-моделей

управляющего автомата, системы вложенных автоматов и системы параллельно работающих автоматов.

3. Изложено предлагаемое в работе расширение LTL-формул и их преобразование к Spin-моделям.

4. Изложен предлагаемый метод верификации автоматных программ.

5. Описаны разработанные автором инструментальные средства для поддержки предложенного метода.

6. Применение предложенного метода продемонстрировано на примере верификации системы автоматов, управляющих гусеничным шасси.