Pascal Raymond
Verification with Lustre/Lesar (2018)
Verification with Lustre/Lesar (2018)
TR-2018-11.pdf
Keywords: Synchronous languages, Model Checking, Safety Properties, Binary Decision Diagrams
Abstract: Synchronous approach has been proposed in the middle of the 80s with the aim of reconcile concurrent programming with determinism. The Lustre language belongs to this approach. It proposes a data-flow programming style, close to classical models like block diagrams or sequential circuits. The semantics of the language is formally defined, and thus formal verification of program functionality is possible. During the 90s, proof methods based on model exploration (model-checking) have been applied with success in domains like protocol or circuit verification. These methods have been adapted for the validation of programs written in the Lustre language, and a specific model-checker (Lesar) has been developed. The first part of this report is dedicated to the presentation of the language and the problems raised by its formal verification: expression of properties and assumptions, conservative abstraction of infinite systems etc. The second part is more general and technical. It details some exploration methods for finite state models. These methods are mainly inspired by previous works on the verification of sequential circuits (symbolic model-checking).
