Step-wise + Algorithmic debugging for Reactive Programs: Ludic, a debugger for Lustre.
Florence Maraninchi, Fabien Gaucher · 2000
For safety-critical reactive systems (in avionics, transportation, nuclear plants, etc.), a lot of effort has been put on the definition of safe languages, with a formal semantics. In the synchronous approach, several languages with distinct programming styles share a common simple view of the world that helps reasoning about programs formally: systems react in zero time. Formal verification and testing tools have been developed, based upon the formal semantics. But there are very few attempts at providing the user with a tool like a debugger. Simulators exist, but they are restricted to the observation of the global inputs and outputs of the reactive system, and to commands like step (on the base clock, for time-triggered implementations) and reset. We would like to provide a real debugger for reactive systems, in the synchronous approach. We are mainly interested in the data-flow language Lustre, for which the distance between the structure of programs and the actual execu...