Verified Compilation of Synchronous Dataflow with State Machines
Article No.: 137, Pages 1 - 26
Abstract
Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.
References
[1]
C. André. 1995. SyncCharts: A Visual Representation of Reactive Behaviors. Technical Report. I3S. RR 95-52.
[2]
C. André. 1996. Representation and analysis of reactive behaviors: A synchronous approach. In Computational Engineering in Systems Applications. 19–29.
[3]
C. Ballabriga, H. Cassé, C. Rochange, and P. Sainrat. 2010. OTAWA: An open toolbox for adaptive WCET analysis. In SEUS(LNCS, Vol. 6399). 35–46.
[4]
A. Benveniste, T. Bourke, B. Caillaud, and M. Pouzet. 2011. Divide and recycle: Types and compilation for a hybrid synchronous language. In LCTES. 61–70.
[5]
G. Berry. 1989. Real time programming: Special purpose or general purpose languages. In IFIP. 11–17.
[6]
G. Berry. 1993. Preemption in concurrent systems. In Foundations of Software Technology and Theoretical Computer Science(LNCS, Vol. 761). 72–93.
[7]
G. Berry and G. Gonthier. 1992. The esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming 19, 2 (1992), 87–152.
[8]
G. Berry, S. Moisan, and J.-P. Rigault. 1983. ESTEREL: Towards a synchronous and semantically sound high level language for real time applications. In RTSS. 30–37.
[9]
D. Biernacki, J.-L. Colaço, G. Hamon, and M. Pouzet. 2008. Clock-directed modular code generation for synchronous data-flow languages. In LCTES. 121–130.
[10]
S. Blazy and X. Leroy. 2009. Mechanized semantics for the clight subset of the C language. JAR 43, 3 (2009), 263–288.
[11]
T. Bourke, L. Brun, P.-É. Dagand, X. Leroy, M. Pouzet, and L. Rieg. 2017. A formally verified compiler for Lustre. In PLDI. 586–601.
[12]
T. Bourke, L. Brun, and M. Pouzet. 2020. Mechanized semantics and verified compilation for a dataflow synchronous language with reset. PACMPL 4, POPL (2020), 1–29.
[13]
T. Bourke, P. Jeanmaire, B. Pesin, and M. Pouzet. 2021. Verified Lustre normalization with node subsampling. ACM TECS 20, 5s (2021), Article 98.
[14]
T. Bourke and M. Pouzet. 2013. Zélus: A synchronous language with ODEs. In HSCC. 113–118.
[15]
P. Caspi. 1992. Clocks in dataflow languages. TCS 94, 1 (1992), 125–140.
[16]
P. Caspi. 1994. Towards recursive block diagrams. Annual Review in Automatic Programming 18 (1994), 81–85.
[17]
P. Caspi, G. Hamon, and M. Pouzet. 2008. Synchronous Functional Programming: The Lucid Synchrone Experiment.
[18]
P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. 1987. LUSTRE: A declarative language for programming synchronous systems. In POPL. 178–188.
[19]
P. Caspi and M. Pouzet. 1998. A co-iterative characterization of synchronous stream functions. In CMCS(ENTCS, Vol. 11).
[20]
J.-L. Colaço, G. Hamon, and M. Pouzet. 2006. Mixing signals and modes in synchronous data-flow systems. In EMSOFT. 73–82.
[21]
J.-L. Colaço, M. Mendler, B. Pauget, and M. Pouzet. 2023. A constructive state-based semantics and interpreter for a synchronous data-flow language with state machines. ACM TECS same issue (2023).
[22]
J.-L. Colaço, B. Pagano, and M. Pouzet. 2005. A conservative extension of synchronous data-flow with state machines. In EMSOFT. 173–182.
[23]
J.-L. Colaço, B. Pagano, and M. Pouzet. 2017. Scade 6: A formal language for embedded critical software development. In TASE. 4–15.
[24]
J.-L. Colaço and M. Pouzet. 2003. Clocks as first class abstract types. In EMSOFT(LNCS, Vol. 2855). 134–155.
[25]
Coq Development Team. 2020. The Coq Proof Assistant Reference Manual. Inria.
[26]
L. Gérard, A. Guatto, C. Pasteur, and M. Pouzet. 2012. A modular memory optimization for synchronous data-flow languages: Application to arrays in a Lustre compiler. In LCTES. 51–60.
[27]
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The synchronous dataflow programming language LUSTRE. Proc. IEEE 79, 9 (1991), 1305–1320.
[28]
G. Hamon. 2002. Calcul d’horloges et structures de contrôle dans Lucid Synchrone, un langage de flots synchrones à la ML. Ph.D. Dissertation. Université Pierre et Marie Curie.
[29]
G. Hamon. 2005. A denotational semantics for stateflow. In EMSOFT. 164–172.
[30]
G. Hamon and M. Pouzet. 2000. Modular resetting of synchronous data-flow programs. In PPDP. 289–300.
[31]
G. Hamon and J. Rushby. 2004. An operational semantics for stateflow. In FASE(LNCS, Vol. 2984). 229–243.
[32]
D. Harel. 1987. Statecharts: A visual formalism for complex systems. Sci. Computer Programming 8, 3 (1987), 231–274.
[33]
R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. 2014. CakeML: A verified implementation of ML. In POPL. 179–191.
[34]
X. Leroy. 2009. Formal verification of a realistic compiler. Comms. ACM 52, 7 (2009), 107–115.
[35]
X. Leroy. 2009. A formally verified compiler back-end. JAR 43, 4 (2009), 363–446.
[36]
F. Maraninchi. 1991. The argos language: Graphical representation of automata and description of reactive systems. In Proc. IEEE Workshop on Visual Languages. 254–259.
[37]
F. Maraninchi and N. Halbwachs. 1996. Compiling argos into boolean equations. In FTRTFT(LNCS, Vol. 1135). 72–89.
[38]
F. Maraninchi and Y. Rémond. 1998. Mode-automata: About modes and states for reactive systems. In ESOP(LNCS, Vol. 1381). 185–189.
[39]
F. Pottier and Y. Régis-Gianas. 2016. Menhir Reference Manual. Inria.
[40]
M. Pouzet. 2006. Lucid Synchrone, v. 3. Tutorial and Reference Manual. Université Paris-Sud.
[41]
L. Rieg and G. Berry. 2022. Towards Coq-verified Esterel Semantics and Compiling. arXiv.
[42]
G. Shi, Y. Gan, S. Shang, S. Wang, Y. Dong, and P.-C. Yew. 2017. A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs. In ICSE-C. 109–111.
[43]
G. Shi, Y. Zhang, S. Shang, S. Wang, Y. Dong, and P.-C. Yew. 2019. A formally verified transformation to unify multiple nested clocks for a Lustre-like language. Science China Information Sciences 62, 1 (2019), no. 12801.
[44]
The Mathworks 2022. Stateflow® User’s Guide (10.7 Ed.). The Mathworks. Matlab & Simulink R2022b.
[45]
J. Zhao, S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. SIGPLAN Not. 47, 1 (2012), 427–440.
Index Terms
- Verified Compilation of Synchronous Dataflow with State Machines
Recommendations
Verified Lustre Normalization with Node Subsampling
Special Issue ESWEEK 2021, CASES 2021, CODES+ISSS 2021 and EMSOFT 2021Dataflow languages allow the specification of reactive systems by mutually recursive stream equations, functions, and boolean activation conditions called clocks. Lustre and Scade are dataflow languages for programming embedded systems. Dataflow programs ...
Mechanized semantics and verified compilation for a dataflow synchronous language with reset
Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that ...
A formally verified compiler for Lustre
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
1394 pages
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Publisher
Association for Computing Machinery
New York, NY, United States
Journal Family
Publication History
Published: 09 September 2023
Accepted: 13 July 2023
Revised: 02 June 2023
Received: 23 March 2023
Published in TECS Volume 22, Issue 5s
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 192Total Downloads
- Downloads (Last 12 months)63
- Downloads (Last 6 weeks)4
Reflects downloads up to 02 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in