Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
Ioannis Parissis , LSR-IMAG, France
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. In this paper, we address two important problems related to 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, due to the often huge required memory and time 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.
I. Parissis, "A Formal Approach to Testing Lustre Specifications," Formal Engineering Methods, International Conference on(ICFEM), Hiroshima, JAPAN, 1997, pp. 91.