Checking experiments with non-observable tree FSMs

Abstract

The paper addresses the problem of deriving preset checking experiments for non-observable FSMs. The fault model is considered to be a ‘white box’ where all possible implementations are explicitly enumerated. We show that if the specification FMS has a tree structure then it is possible to derive a complete checking experiment that has polynomial length.

Keywords

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