Сборники трудов ИСП РАН


Проверяющие эксперименты с ненаблюдаемым древовидными автоматами

Н.Г. Кушик (Телеком Южный Париж, Франция)

Аннотация

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

Ключевые слова

конечный автомат, недетерминированный (ненаблюдаемый) автомат, древовидный автомат, проверяющий эксперимент

Издание

Труды Института системного программирования РАН, том 27, вып. 6, 2015, стр. 441-450.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2015-27(6)-28

Полный текст статьи в формате pdf Вернуться к содержанию тома