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 carl be proven by model-checking, using LESAR, a verification tool designed for LUSTRE programs. In this paper; we address two important problems related ro this verification process. First, developing the specifications of a 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, dire to the often huge required memory and rime amounts, 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.