Верификация автоматных программ с использованием LTL

Рассматривается один из способов моделирования, спецификации и верификации программ, построенных на основе автоматного подхода к программированию. Технология автоматного программирования является достаточно эффективной при создании программного обеспечения для «реактивных» систем и систем логического управления. С точки зрения моделирования и анализа программных систем эта технология имеет ряд преимуществ по сравнению с традиционным подходом, так как исключает проблему адекватности построенной программной модели исходной программе. Набор взаимодействующих автоматов, описывающий логику программы, уже является адекватной моделью, по которой формальным образом строится программный модуль. Свойства программной системы в виде автоматов могут быть сформулированы и специфицированы естественным и понятным образом. Проверка свойств осуществляется в терминах, которые естественно вытекают из автоматной модели программы. Практическим результатом работы является применение инструментального средства SPIN и логики LTL для спецификации и верификации иерархических автоматных программ.