Teaching Synchronous Dataflow Modelling with Learn-Heptagon
2026-06-01 • Programming Languages
Programming Languages
AI summaryⓘ
The authors explain Lustre, a programming language used for creating and checking safety-critical software. They highlight that Lustre can both run programs and serve as a way to describe and verify the program's expected behavior. To help students learn Lustre more easily, the authors developed an online tool called Learn-Heptagon that lets users write, test, and prove properties of Lustre programs. They also share the lesson plan they used alongside this tool for teaching engineering students.
Lustresynchronous dataflowembedded softwaresynchronous observersassume-guarantee contractsmodel checkingprogram logicsimulationsafety-critical systemsonline learning tool
Authors
Pierre-Loïc Garoche, Basile Pesin
Abstract
Lustre is a synchronous dataflow language designed to implement safety-critical embedded software. In addition to writing executable programs, the language doubles as a program logic, used for writing specification as synchronous observers or assume-guarantee contracts that specify properties of these programs. These specifications may be used during testing or proved exhaustively using model-checking tools. We taught a course on Lustre to last year engineering students. To streamline the learning experience and avoid technical issues, we developped an online application, Learn-Heptagon, which allows for writing, simulating, and proving properties of Lustre programs. This paper presents the application and the associated lesson plan.