Presentation
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: complex programs and properties, in particular those involving numerical aspects.
Any language that compiles into C, and that has an explicit notion of step ought to be used with minor modifications to Lurette.
The main ideas behind Lurette are described in [1]. A first prototype was designed at that point. Lurette was then completely re-implemented. The main difference is that we now use Lucky (instead of Lustre) to specify the the System Under Test (SUT) environment constraints. This work was sponsored by the SAFEAIR II IST project.
Lurette has also been used in the ASSERT project and in the COMON project.
Documents
— The first paper describing the principles of Lurette
— A paper describing case studies conducted with Lurette [2]
— The Lurette User Guide
— The Lutin page
— The Download page
