Аннотация:Целью данной работы является разработка и исследования способов интеграции системы верификации SPIN в среду ДИАНА.
Для достижения данной цели в рамках работы решены следующие задачи:
* Разработка алгоритмов отображения моделей, разработанных в среде ДИАНА, на язык PROMELA.
* Реализация разработанных алгоритмов.
* Обоснование корректности разработанных алгоритмов.
* Исследование эффективности и оптимизации построенных алгоритмов.
Приведённые в работе результаты исследования показали высокую эффективность разработанных алгоритмов и доказали возможность использования системы верификации на основе средства SPIN для проверки реальных иммитационных моделей.