Formal passive testing of timed systems: theory and tools

This paper presents a methodology to perform passive testing of timed systems. In passive testing, the tester does not interact with the implementation under test. On the contrary, execution traces are observed without interfering with the behaviour of the system. Invariants are used to represent the most relevant expected properties of the implementation under test. Intuitively, an invariant expresses the fact that each time the implementation under test performs a given sequence of actions, it must exhibit a behaviour in a lapse of time reflected in the invariant. There are two types of invariants: consequent and observational. The paper gives two algorithms to decide the correctness of proposed invariants with respect to a given specification and algorithms to check the correctness of a log, recorded from the implementation under test, with respect to an invariant. The soundness of this methodology is shown by relating it to an implementation relation. In addition to the theoretical framework, a tool called PASTE has been developed. This tool helps in the automation of the passive testing approach because it implements all the algorithms presented in this paper. PASTE takes advantage of mutation testing techniques in order to evaluate the goodness of an invariant according to its capability to detect errors in logs generated from mutants. An empirical study where PASTE was used to analyse a non-trivial system is also reported. Copyright (C) 2012 John Wiley & Sons, Ltd.