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