Presentation
The main challenge in automating a testing or a simulation process is to be able to automate the generation of realistic input sequences to feed the program. In other words, we need an executable model of the program environment for which inputs are the program outputs, and for which outputs are the program inputs.
In the first Lurette prototype (an automated testing tool for reactive programs designed at Verimag), the System Under Test (SUT) environment behavior was described by Lustre observers which specified the form of realistic SUT inputs. In other words, the environment was modeled by a set of (linear) constraints over Boolean and numeric variables. The work of Lurette was to solve those constraints, and to draw a value among the solutions to produce one SUT input vector.
However, Lustre observers happen to be too restrictive, in particular to express sequences of different testing scenarios, or to have some control on the probabilistic distribution of the drawn solution. It was precisely to overcome those limitations that a new language, Lutin, was designed. Lutin can be compiled into an intermediate format called Lucky.
— Lutin is core component of Lurette Lutin
— We use Lucky to help Nbac find concrete counter-examples when proofs fail See the AADEBUG’03 paper.
— LuckyDraw, provides a direct access to the Lucky solver and drawer from Ocaml (and soon, to C) libraries. It is used at IRISA in the Vertecs team for the STG tool.
— Luc4ocaml lets one use Lutin or Lucky programs from ocaml. This library is used in particular by Reactive ML.
Documents
— The Lutin Manual.
— A Lutin tutorial in pdf and in html
— The Download page
