Checking Experiments with Non-Observable Tree FSMs
The paper addresses the problem of deriving preset checking experiments for non-observable Finite State Machines (FSMs). This problem often appears when checking functional and non-functional requirements of various discrete and hybrid systems. In this case, the model of an FSM is adequate as it allows to formally describe systems with finite non-empty sets of states and finite sets of inputs and outputs that move from one state to another when an input is applied and an output is produced. Checking experiments, on the other hand, allow to verify if a given FSM conforms to another one or not. When deriving checking experiments for nondeterministic FSMs, different conformance relations can be considered as well as different ways to define the set of faulty implementations which the experiment aims to detect. In this paper, we consider a non-separability relation, and the fault model is considered to be a ‘white box’ where all possible implementations are explicitly enumerated. Faulty implementations can contain first order transfer and output faults. Non-separability relation requires that two initialized machines have at least one common output reaction to any input sequence. In the paper, we define a specific class of fault models such that the checking experiment that detects each implementation not conforming to the specification has polynomial length. In particular, we show that if the specification FSM has a tree structure then it is possible to derive a complete checking experiment that has polynomial length.
Proceedings of the Institute for System Programming, vol. 27, issue 6, 2015, pp. 441-450.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).
DOI: 10.15514/ISPRAS-2015-27(6)-28Full text of the paper in pdf (in Russian) Back to the contents of the volume