Erwan Jahier, Pascal Raymond
The Lucky language Reference Manual (2004)
The Lucky language Reference Manual (2004)
TR-2004-6.pdf
Keywords: Reactive systems, validation, automatic test case generation, lurette, lustre
Abstract: The main challenge to automate 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 which inputs are the program outputs, and which outputs are the program inputs. In the first Lurette prototype -- an automated testing tool of reactive programs designed at Verimag --, the System Under Test (SUT) environment behaviour was described by Lustre observers which were specifying what realistic SUT inputs should be. In other words, the environment was modelled 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. But, from a language expressing power point of view, 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, Lucky, was designed. A Lucky program is an interpreted automaton whose transitions define the reactions of the machine. More precisely, each transition is associated to (1) a set of constraints (a lustre-like formula) that defines the set of the possible outputs, and (2) a weight that defines the relative probability for each transitions to be taken, i.e., to be used to produce the output vector for the current step.
