Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing

Abstract:
This paper surveys the techniques and tools developped for the validation of reactive systems described in the synchronous data-flow language Lustre. These techniques are based on the specification of safety properties, by means of synchronous observers. The model-checker Lesar takes a Lustre program, and two observers --- respectively describing the expected properties of the program, and the assumptions about the system environment under which these properties are intended to hold ---, and performs the verification on a finite state (Boolean) abstraction of the system. Recent work concerns extensions towards simple numerical aspects, which are ignored in the basic tool. Provided with the same kind of observers, the tool Lurette is able to automatically generate test sequences satisfying the environment assumptions, and to run the test while checking the satisfaction of the specified properties.

Reference:

@inproceedings{asian99,
author = {N. Halbwachs and P. Raymond},
title = {Validation of Synchronous Reactive Systems:
from Formal Verification to Automatic Testing},
booktitle = {ASIAN'99, Asian Computing Science Conference},
publisher={LNCS 1742, Springer Verlag},
address={Phuket (Thailand)},
year = 1999,
month = dec
}

Postscript file