pith. sign in

arxiv: 2606.01928 · v1 · pith:UPM3DRX6new · submitted 2026-06-01 · 💻 cs.PL

Teaching Synchronous Dataflow Modelling with Learn-Heptagon

Pierre-Lo\"ic Garoche , Basile Pesin This is my paper

Pith reviewed 2026-06-28 12:06 UTC · model grok-4.3

classification 💻 cs.PL
keywords Lustresynchronous dataflowonline learning toolmodel checkingembedded softwareformal specificationteaching programming languages
0
0 comments X

The pith

Learn-Heptagon provides an online environment for writing, simulating, and model-checking Lustre programs in a browser.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Learn-Heptagon, an online application developed to teach Lustre, a synchronous dataflow language for safety-critical embedded software. Lustre programs can also serve as specifications through synchronous observers or assume-guarantee contracts, which support testing or exhaustive proof via model checking. The tool combines editing, execution simulation, and property proving to reduce setup barriers for students. It was paired with a dedicated lesson plan and used in a course for final-year engineering students.

Core claim

We developed Learn-Heptagon, an online application that allows for writing, simulating, and proving properties of Lustre programs, and we present this application together with the associated lesson plan used to teach synchronous dataflow modelling to engineering students.

What carries the argument

Learn-Heptagon, an online platform that integrates program editing, simulation of synchronous dataflow execution, and model-checking of properties expressed as observers or contracts.

Load-bearing premise

An online application of this kind will in fact streamline the learning experience and avoid technical issues for the target student population.

What would settle it

A controlled comparison in which students using local Lustre installations complete the same assignments with equal or fewer setup problems and comparable or better learning outcomes than those using Learn-Heptagon.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper describes the development of Learn-Heptagon, an online web application allowing users to write, simulate, and prove properties of Lustre programs (via synchronous observers and assume-guarantee contracts), together with the lesson plan employed in a course on synchronous dataflow modelling taught to final-year engineering students. The stated motivation is to reduce technical setup friction compared with local installations of Lustre/Heptagon tooling.

Significance. The work supplies a concrete, immediately usable teaching artifact for a safety-critical language whose model-checking and contract features are otherwise difficult for novices to access. By bundling editing, simulation, and property proving in a single browser-based interface, the tool addresses a genuine pedagogical pain point; the accompanying lesson plan further documents how these features can be sequenced in a classroom setting. These are modest but tangible contributions to the literature on domain-specific-language education.

minor comments (1)
  1. [Abstract] Abstract: 'developped' is a typographical error and should read 'developed'.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, the recognition of the pedagogical contributions of Learn-Heptagon, and the recommendation to accept the manuscript.

Circularity Check

0 steps flagged

No significant circularity; purely descriptive report

full rationale

The paper contains no derivations, equations, predictions, fitted parameters, or load-bearing self-citations. Its content is limited to describing the development of the Learn-Heptagon online tool for Lustre programs and presenting an associated lesson plan. The abstract and full text frame this as a straightforward report of tool creation and course delivery, with no claims that reduce to inputs by construction or rely on unverified self-referential premises. This matches the default expectation of a non-circular paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a descriptive account of software-tool development and course design; it introduces no mathematical parameters, background axioms, or postulated entities.

pith-pipeline@v0.9.1-grok · 5627 in / 1001 out tokens · 30309 ms · 2026-06-28T12:06:26.029615+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

300 extracted references · 37 canonical work pages

  1. [1]

    Timothy Bourke , title =

  2. [2]

    doi:10.1142/S0218194005002300 , url =

    Timothy Bourke and Arcot Sowmya , title =. doi:10.1142/S0218194005002300 , url =

    work page doi:10.1142/s0218194005002300

  3. [3]

    doi:10.1145/1176887.1176901 , url =

    Timothy Bourke and Arcot Sowmya , title =. doi:10.1145/1176887.1176901 , url =

    work page doi:10.1145/1176887.1176901

  4. [4]

    Leonid Ryzhyk and Timothy Bourke and Ihor Kuz , title =

  5. [5]

    doi:10.1145/1450058.1450068 , url =

    Timothy Bourke and Arcot Sowmya , title =. doi:10.1145/1450058.1450068 , url =

    work page doi:10.1145/1450058.1450068

  6. [6]

    Timothy Bourke and Arcot Sowmya , title =

  7. [7]

    Larsen and Axel Legay and Didier Lime and Ulrik Nyman and Andrzej W

    Timothy Bourke and Alexandre David and Kim G. Larsen and Axel Legay and Didier Lime and Ulrik Nyman and Andrzej W. New Results on Timed Specifications , booktitle =. doi:10.1007/978-3-642-28412-0_12 , url =

    work page doi:10.1007/978-3-642-28412-0_12

  8. [8]

    Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language , crossref =

    Albert Benveniste and Timothy Bourke and Beno. Divide and Recycle: Types and Compilation for a Hybrid Synchronous Language , crossref =. doi:10.1145/1967677.1967687 , url =

    work page doi:10.1145/1967677.1967687

  9. [9]

    Structural

    Papailiopoulou, Virginia and Rajan, Ajitha and Parissis, Ioannis , editor =. Structural. Formal. doi:10.1007/978-3-642-24431-5_8 , abstract =

    work page doi:10.1007/978-3-642-24431-5_8

  10. [10]

    Non-Standard Semantics of Hybrid Systems Modelers , journal = jcss, year = 2012, month = may, volume = 78, number = 3, pages =

    Albert Benveniste and Timothy Bourke and Beno. Non-Standard Semantics of Hybrid Systems Modelers , journal = jcss, year = 2012, month = may, volume = 78, number = 3, pages =. doi:10.1016/j.jcss.2011.08.009 , url =

    work page doi:10.1016/j.jcss.2011.08.009 2012

  11. [11]

    A Hybrid Synchronous Language with Hierarchical Automata: Static Typing and Translation to Synchronous Code , crossref =

    Albert Benveniste and Timothy Bourke and Beno. A Hybrid Synchronous Language with Hierarchical Automata: Static Typing and Translation to Synchronous Code , crossref =. doi:10.1145/2038642.2038664 , url =

    work page doi:10.1145/2038642.2038664

  12. [12]

    Conferences on Intelligent Computer Mathematics (CICM 2012): Mathematical Knowledge Management , year = 2012, editor =

    Timothy Bourke and Matthias Daum and Gerwin Klein and Rafal Kolanski , title =. Conferences on Intelligent Computer Mathematics (CICM 2012): Mathematical Knowledge Management , year = 2012, editor =. doi:10.1007/978-3-642-31374-5_3 , url =

    work page doi:10.1007/978-3-642-31374-5_3 2012

  13. [13]

    doi:10.1145/2461328.2461348 , url =

    Timothy Bourke and Marc Pouzet , title =. doi:10.1145/2461328.2461348 , url =

    work page doi:10.1145/2461328.2461348

  14. [14]

    doi:10.1145/2539036.2539040 , url =

    Timothy Bourke and Arcot Sowmya , title =. doi:10.1145/2539036.2539040 , url =

    work page doi:10.1145/2539036.2539040

  15. [15]

    doi:10.1109/SP.2013.35 , url =

    Toby Murray and Daniel Matichuk and Matthew Brassil and Peter Gammie and Timothy Bourke and Sean Seefried and Corey Lewis and Xin Gao and Gerwin Klein , title =. doi:10.1109/SP.2013.35 , url =

    work page doi:10.1109/sp.2013.35 2013

  16. [16]

    doi:10.1145/2562059.2562125 , url =

    Albert Benveniste and Timothy Bourke and Benoit Caillaud and Bruno Pagano and Marc Pouzet , title =. doi:10.1145/2562059.2562125 , url =

    work page doi:10.1145/2562059.2562125

  17. [17]

    Bourke, Timothy and van Glabbeek, Robert J. and H. Showing invariance compositionally for a process algebra for network protocols , crossref =. doi:10.1007/978-3-319-08970-6_10 , url =

    work page doi:10.1007/978-3-319-08970-6_10

  18. [18]

    Bourke, Timothy , journal = afp, title =

  19. [19]

    Bourke, Timothy and van Glabbeek, Robert J. and H. A mechanized proof of loop freedom of the (untimed). doi:10.1007/978-3-319-11936-6_5 , url =

    work page doi:10.1007/978-3-319-11936-6_5

  20. [20]

    Loop freedom of the (untimed)

    Bourke, Timothy and H. Loop freedom of the (untimed)

  21. [21]

    A Synchronous-based Code Generator for Explicit Hybrid Systems Languages , booktitle = cc2015, year = 2015, pages =

    Timothy Bourke and Jean-Louis Cola. A Synchronous-based Code Generator for Explicit Hybrid Systems Languages , booktitle = cc2015, year = 2015, pages =. doi:10.1007/978-3-662-46663-6_4 , url =

    work page doi:10.1007/978-3-662-46663-6_4 2015

  22. [22]

    Bourke, Timothy and van Glabbeek, Robert J. and H. Mechanizing a Process Algebra for Network Protocols , journal = jar, year = 2016, volume = 56, number = 3, pages =. doi:10.1007/s10817-015-9358-9 , url =

    work page doi:10.1007/s10817-015-9358-9 2016

  23. [23]

    doi:10.1109/EMSOFT.2015.7318263 , url =

    Guillaume Baudart and Albert Benveniste and Timothy Bourke , title =. doi:10.1109/EMSOFT.2015.7318263 , url =

    work page doi:10.1109/emsoft.2015.7318263 2015

  24. [24]

    doi:10.1145/2932189 , url =

    Guillaume Baudart and Albert Benveniste and Timothy Bourke , title =. doi:10.1145/2932189 , url =

    work page doi:10.1145/2932189

  25. [25]

    doi:10.1109/FMCAD.2016.7886655 , url =

    Guillaume Baudart and Timothy Bourke and Marc Pouzet , title =. doi:10.1109/FMCAD.2016.7886655 , url =

    work page doi:10.1109/fmcad.2016.7886655 2016

  26. [26]

    ACM Workshop on ML , year = 2016, month = sep, organization =acm, address =

    Timothy Bourke and Jun Inoue and Marc Pouzet , title =. ACM Workshop on ML , year = 2016, month = sep, organization =acm, address =

    2016

  27. [27]

    Timothy Bourke and Pierre-. V

  28. [28]

    A Formally Verified Compiler for

    Timothy Bourke and L. A Formally Verified Compiler for. doi:10.1145/3062341.3062358 , url =

    work page doi:10.1145/3062341.3062358

  29. [29]

    A type-based analysis of causality loops in hybrid systems modelers , journal = nahs, year = 2017, month = nov, pages =

    Albert Benveniste and Timothy Bourke and Beno. A type-based analysis of causality loops in hybrid systems modelers , journal = nahs, year = 2017, month = nov, pages =. doi:10.1016/j.nahs.2017.04.004 , url =

    work page doi:10.1016/j.nahs.2017.04.004 2017

  30. [30]

    Guillaume Baudart and Timothy Bourke and Marc Pouzet , title =

  31. [31]

    A Synchronous Look at the

    Timothy Bourke and Francois Carcenac and Jean-Louis Cola. A Synchronous Look at the. doi:10.1145/3126516 , url =

    work page doi:10.1145/3126516

  32. [32]

    Jean Souyris and Keryan Didier and Dumitru Potop and Guillaume Iooss and Albert Cohen and Timothy Bourke and Marc Pouzet , title =

  33. [33]

    doi:10.4204/EPTCS.285.4 , url =

    Timothy Bourke and Jun Inoue and Marc Pouzet , title =. doi:10.4204/EPTCS.285.4 , url =

    work page doi:10.4204/eptcs.285.4

  34. [34]

    Towards a verified Lustre compiler with modular reset , pages =

    Timothy Bourke and L. Towards a verified Lustre compiler with modular reset , pages =

  35. [35]

    Building a Hybrid Systems Modeler on Synchronous Languages Principles , journal = procieee, year = 2018, month = sep, pages =

    Albert Benveniste and Timothy Bourke and Benoit Caillaud and Jean-Louis Cola. Building a Hybrid Systems Modeler on Synchronous Languages Principles , journal = procieee, year = 2018, month = sep, pages =. doi:10.1109/JPROC.2018.2858016 , url =

    work page doi:10.1109/jproc.2018.2858016 2018

  36. [36]

    Languages, Design Methods, and Tools for Electronic System Design: Selected Contributions from FDL 2017 , editor =

    Guillaume Baudart and Timothy Bourke and Marc Pouzet , title =. Languages, Design Methods, and Tools for Electronic System Design: Selected Contributions from FDL 2017 , editor =. doi:10.1007/978-3-030-02215-0_3 , url =

    work page doi:10.1007/978-3-030-02215-0_3 2017

  37. [37]

    Timothy Bourke and Marc Pouzet , title =

  38. [38]

    Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset , journal = papl, publisher = acmpress, volume = 4, number =

    Timothy Bourke and L. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset , journal = papl, publisher = acmpress, volume = 4, number =. doi:10.1145/3371112 , url =

    work page doi:10.1145/3371112

  39. [39]

    2021 , month = oct, pages =

    Timothy Bourke and Paul Jeanmaire and Basile Pesin and Marc Pouzet , title =. 2021 , month = oct, pages =. doi:10.1145/3477041 , keywords =

    work page doi:10.1145/3477041 2021

  40. [40]

    Analyse de d

    Timothy Bourke and Basile Pesin and Marc Pouzet , pages =. Analyse de d

  41. [41]

    doi:10.1145/3608102 , url =

    Verified Compilation of Synchronous Dataflow with State Machines , author =. doi:10.1145/3608102 , url =

    work page doi:10.1145/3608102

  42. [42]

    Functional Stream Semantics for a Synchronous Block-Diagram Compiler , author =

  43. [43]

    Guillaume Baudart , title =

  44. [44]

    Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset , school =

    L. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset , school =

  45. [45]

    Basile Pesin , title =

  46. [46]

    Paul Jeanmaire , title =

  47. [47]

    Guillaume Iooss and Marc Pouzet and Timothy Bourke , title =

  48. [48]

    Lee , title =

    Edward A. Lee , title =. IEEE Computer , year = 2000, volume = 33, number = 9, pages =

    2000

  49. [49]

    Alan Burns , title =

  50. [50]

    Harel and A

    D. Harel and A. Pnueli , title =. Logics and models of concurrent systems , year = 1985, isbn =

    1985

  51. [51]

    Preemption in Concurrent Systems , booktitle = fsttcs, year = 1993, month = dec, editor =

    G\'. Preemption in Concurrent Systems , booktitle = fsttcs, year = 1993, month = dec, editor =

    1993

  52. [52]

    Science of Computer Programming , volume = 8, number = 3, month = jun, pages =

    David Harel , title =. Science of Computer Programming , volume = 8, number = 3, month = jun, pages =

  53. [53]

    Harel and A

    D. Harel and A. Pnuelli and J.P. Schmidt and R. Sherman , title =. 2nd IEEE Symposium on Logic in Computer Science , year = 1987, review =

    1987

  54. [54]

    Formal Techniques in Real-Time and Fault-Tolerant Systems , year =

    Michael von der Beeck , title =. Formal Techniques in Real-Time and Fault-Tolerant Systems , year =

  55. [55]

    David Harel and Amnon Naamad , title =

  56. [56]

    Harel and H

    D. Harel and H. Lachover and A. Naamad and A. Pnueli and M. Politi and R. Sherman and A. Shtull-Trauring and M. Trakhtenbrot , title =

  57. [57]

    Leveson and Mats Per Erik Heimdahl and Holly Hildreth and Jon Damon Reese , title =

    Nancy G. Leveson and Mats Per Erik Heimdahl and Holly Hildreth and Jon Damon Reese , title =

  58. [58]

    von Hanxleden, Reinhard and Botorabi, Ali and Kupczyk, Slawomir , title =

  59. [59]

    David Harel , title =

  60. [60]

    Mikk and Y

    E. Mikk and Y. Lakhnech and C. Petersohn and M. Siegel , title =. 2nd BCS-FACS Northern Formal Methods Workshop , year = 1997, address =

    1997

  61. [61]

    Stefania Gnesi and Diego Latella and Mieke Massink , title =

  62. [62]

    A Compositional Approach to Statecharts Semantics , booktitle = FSE8, pages =

    Gerald L. A Compositional Approach to Statecharts Semantics , booktitle = FSE8, pages =

  63. [63]

    The intuitionism behind Statecharts steps , journal = tocl, year = 2002, volume = 3, number = 1, pages =

    Gerald L. The intuitionism behind Statecharts steps , journal = tocl, year = 2002, volume = 3, number = 1, pages =

    2002

  64. [64]

    Werner Damm and Bernhard Josko and Hardi Hungar and Amir Pnueli , title =

  65. [65]

    The Synchronous Approach to Reactive and Real-Time Systems , journal = procieee, year = 1991, VOLUME= 79, number = 9, pages =

    Albert Benveniste and G\'. The Synchronous Approach to Reactive and Real-Time Systems , journal = procieee, year = 1991, VOLUME= 79, number = 9, pages =

    1991

  66. [66]

    Benveniste, Albert and Caspi, Paul and Edwards, Stephen and Halbwachs, Nicolas and Le Guernic, Paul and de Simone, Robert , title =

  67. [67]

    Synchronous Programming of Reactive Systems

    Nicolas Halbwachs. Synchronous Programming of Reactive Systems

  68. [68]

    Real Time Programming: Special Purpose or General Purpose Languages , booktitle = ifip89, year = 1989, editor =

    G. Real Time Programming: Special Purpose or General Purpose Languages , booktitle = ifip89, year = 1989, editor =

    1989

  69. [69]

    Timing analysis enhancement for synchronous program , journal = rts, volume = 51, number = 2, pages =

    Pascal Raymond and Claire Maiza and Catherine Parent. Timing analysis enhancement for synchronous program , journal = rts, volume = 51, number = 2, pages =

  70. [70]

    ESTEREL: Towards a synchronous and semantically sound high level language for Real Time Applications , crossref =

    G\'. ESTEREL: Towards a synchronous and semantically sound high level language for Real Time Applications , crossref =

  71. [71]

    Esterel Technologies , organization =. The

  72. [72]

    The Foundations of

    G\'. The Foundations of. Proof, Language and Interaction: Essays in Honour of Robin Milner , year = 2000, editor =

    2000

  73. [73]

    G\'. The. Seminar on Concurrency , series = lncs, volume = 197, pages =

  74. [74]

    G\'. The. doi:10.1016/0167-6423(92)90005-V , url =

    work page doi:10.1016/0167-6423(92)90005-v

  75. [75]

    The Constructive Semantics of Pure Esterel , year = 2002, url =

    G\'. The Constructive Semantics of Pure Esterel , year = 2002, url =

    2002

  76. [76]

    Tardieu, Olivier and de Simone, Robert , title =

  77. [77]

    Olivier Tardieu , title =

  78. [78]

    Edwards and Edward A

    Stephen A. Edwards and Edward A. Lee , title =

  79. [79]

    Shyamasundar , title =

    Basant Rajan and R.K. Shyamasundar , title =

  80. [80]

    Martin Richard and Olivier Roux , title =

Showing first 80 references.