Патенты автора Петренко Александр Константинович (RU)
Изобретение относится к способу верификации формальной автоматной модели поведения программной системы. Технический результат заключается в автоматизации проверки корректности верифицируемой автоматной модели. В способе при построении более простой автоматной модели выделяют подмножество переменных верифицируемой формальной автоматной модели так, чтобы часть ее событий изменяла только переменные, не входящие в это подмножество, используют переменные, инварианты и начальные состояния более простой автоматной модели, разбивают события верифицируемой формальной автоматной модели на цепочки более простых действий, проверяют предусловия и постусловия событий в каждой цепочке, проверяют выполнение инвариантов более простой автоматной модели во всех ее состояниях, проверяют выполнение инвариантов верифицируемой формальной автоматной модели в ее начальных состояниях, проверяют выполнение во всех состояниях инвариантов верифицируемой формальной автоматной модели, не входящих в простую модель, и по результатам проверок делают заключение о корректности верифицируемой модели. 1 з.п. ф-лы, 2 ил.
