Erwan Jahier
The Lurette V2 User Guide (2004)
The Lurette V2 User Guide (2004)
TR-2004-5.pdf
Keywords: Reactive systems, validation, automatic test case generation, lurette, lustre
Abstract: Lurette is an Automatic Test Generator for Reactive Programs . It is automated in two main ways. Realistic input sequences are generated from non-deterministic formal descriptions of the System Under Test Environment properties (pre-conditions). The test decision is done with a formal description of the desired properties -- correct behaviours -- of the SUT (post-conditions). Of course, formal verification should be used whenever possible. However, because program verification is undecidable, testing will always be necessary. Lurette therefore concentrates on cases where formal verification is limited: programs and complex properties, in particular involving numerical aspects. Lurette has been redesigned from scratch. This document is a User Guide for this new version of Lurette. Its provides an -- hopefully -- exhaustive description of its features, as well as a tutorial.
