Automatic testing of reactive systems

The paper addresses the problem of automatizing the production of test sequences for reactive systems. We particularly focus on two points: (1) generating relevant inputs, with respect to some knowledge about the environment in which the system is intended to run; (2) checking the correctness of the test results, according to the expected behavior of the system. We propose to use synchronous observers to express both the relevance and the correctness of the test sequences. In particular, the relevance observer is used to randomly choose inputs satisfying temporal assumptions about the environment. These assumptions may involve both Boolean and linear numerical constraints. A prototype tool called LURETTE has been developed and experimented with, which works on observers written in the LUSTRE programming language