Заключение

В работе получены следующие научные результаты:

• обоснован выбор математических моделей управляющих автоматов;

• разработаны алгоритмы построения Spin-моделей для одного автомата, системы вложенных автоматов (иерархического автомата) и системы параллельно работающих иерархических автоматов;

• разработан метод верификации автоматных программ: построение Spin- модели, преобразование расширенныхLTL-формул в Spin-формулы, преобразование контрпримера в путь в системе автоматов;

• разработан подход для верификации программ в случаях, когда модель внешней среды нельзя представить в виде автомата, например, для клетчатого поля неограниченных размеров.

Также автором разработаны инструментальные средства для верификации автоматных программ разных типов. Результаты работы внедрены в практику разработки ПО и в учебный процесс на кафедре «Компьютерные технологии» Университета ИТМО. Акты о внедрении и использовании имеются.