?
ЭКСПЕРИМЕНТАЛЬНОЕ СРАВНЕНИЕ МЕТОДОВ ПРОВЕРКИ ЭКВИВАЛЕНТНОСТИ РАСШИРЕННЫХ ПОЛУАВТОМАТОВ
В данной работе были рассмотрены две группы приближённых подходов к проверке эквивалентности расширенных полуавтоматов, основанные на использовании классической абстракции (l-эквивалента), поведение которой совпадает с таковым для исходного полуавтомата для всех последовательностей длины не больше l. Идея подходов первой группы заключается в построении для абстракции расширенного полуавтомата некоторого конечного множества трасс и поиске в нем трассы, принимаемой одним полуавтоматом и не принимаемой другим, эквивалентность которого первому полуавтомату требуется проверить. В качестве множества таких трасс были рассмотрены последовательности, полученные обходом графа переходов классического полуавтомата, а также, все простые пути из начального состояния в любое из финальных состояний. Ко второй группе подходов относится проверка свойств исследуемых автоматов с использованием верификаторов. В логике линейного времени (LTL) формулируется свойство, согласно которому любое из финальных состояний в каждом из полуавтоматов достигается одновременно при выполнении любой входной трассы. В настоящей работе использовался верификатор Spin, который позволяет проверять требования, заданные в виде LTL-формул для систем, описанных на языке Promela.