A formal approach to testing LUSTRE specifications

LUSTRE is a synchronous declarative language designed to specify and to implement reactive software. One of its main advantages is that it can be used as a temporal logic to express software invariant properties. The satisfaction of the latter can be proven by model-checking, using LESAR, a verification tool designed for LUSTRE programs. We address two important problems related to this verification process. First, developing the specifications of synchronous software is a difficult and error-prone task. Before attempting to formally prove their satisfaction, one should validate them. We propose random automatic animation as a means to validate such formal specifications. Second, due to the often huge amounts of required memory and time, proof may not be applicable, in which case the specification work is wasted. To cope with this problem, we propose testing techniques which reuse the software specifications to formally test the software.