Alexandre Petrenko

The paper addresses the problems of active learning and conformance testing of systems modeled by nondeterministic Mealy machines (NFSM). It presents a unified SAT-based approach originally proposed by the authors for deterministic FSMs and now generalized to partial nondeterministic machines and checking experiments. Learning a nondeterministic black box, the approach neither needs a Teacher nor uses it a conformance tester to approximate equivalence queries. The idea behind this approach is to infer from a current set of traces not one, but two inequivalent conjectures, use an input sequence distinguishing them in an output query, and update the current trace set with an observed trace to obtain a new pair of distinguishable conjectures, if possible. The classical active learning problem is further generalized by adding a nondeterministic specification FSM, which defines the solution space. The setup unifies the learning and adaptive testing problems and makes them equisolvable with the proposed approach.

Test oracles are usually used to evaluate the behaviors of systems under test to reveal faults. In a typical conformance testing scenario, a test oracle is a deterministic finite state machine (FSM). However, uncertainty occurring in the design of an oracle may result in a set of potential candidate oracles which can compactly be represented by a nondeterministic FSM thus modelling an imprecise test oracle. In the context of testing deterministic systems, such an oracle should ideally be reduced to a precise, i.e., deterministic oracle. We elaborate two scenarios for dealing with imprecise test oracles that involve a domain expert playing the role of an "ultimate" oracle. In the first scenario, the expert chooses a right oracle by inspecting the generated tests differentiating all potential precise oracles which can be derived from a given imprecise one. In the second scenario, the expert evaluates tests one by one while they are generated, and the imprecise oracle is iteratively reduced until a single precise oracle remains, if at all.