Precision-Timed Synchronous Reactive Processing
Final Report Abstract
Safety-critical and cyber-physical systems, e. g., in the domains of avionics, automotive, healthcare or plant control, impose high demands on the functional correctness and timing predictability of embedded software. To achieve such strong correctness guarantees, software engineering has been developing a range of sound approaches such as automatic verification, real-time analysis and hybrid system modelling. The PREcision Time SYnchronous Processing (PRETSY) project explored a new holistic methodology for embedded system development combining domain-specific synchronous programming languages and dedicated precision-timed architectures. The synchronous programming model provides mathematically clean, simple and deterministic semantics. Precision-timed processing architectures provide predictable and controllable timing behaviour. By integrating these independent developments, the PRETSY approach was able to make a number of important advances. In particular, PRETSY developed novel synchronous principles for modelling and programming, static analyses for schedulability and worst-case reaction time. PRETSY also delivered a semantically coherent tool chain for correct-by-construction compilation from a high-level synchronous language to low-level code on precision-timed architectures. Besides PRETSY consolidated the new Sequential Constructiveness (SC) model of computation as a key enabler to reconcile the declarative synchronous programming approach with mainstream imperative embedded programming. Under SC the programmer can employ shared memory for communicating concurrent processes (threads) and still destructively update (re-write) the memory in a race-free manner during a single clock tick. As a result of this memory reuse, SC supports the execution of more code per synchronous cycle without sacrificing the guarantee of deterministic execution. On top of this, PRETSY has taken a major step towards object-based programming for SP by means of the SC generalisaton to the model of Policy-Synchronised Shared Memory. This provides, for the first time, support for data abstraction and general abstract data types in SP approaching SP to main-stream programming, particularly for concurrent applications. In addition, we provide a compositional model for timing interfaces to be used in what we call Interactive WCET Timing Analysis. Our WCRT algebra provides a novel timing-enriched semantics for synchronous programs. It allows us to express in a single formalism both the functional and the timing behaviour of SC programs. It support timing and data-abstraction and thus can be used as an efficient computational basis for timing analysis algorithms. The PRETSY project has brought about two new modeling languages SCEst and SCCharts, that extend the classic synchronous languages Esterel and SyncCharts with sequential constructiveness. These extensions simplify synchronous programming significantly, by allowing more compact models/programs and making causality errors less likely. The practicality of that approach has been demonstrated throughout numerous student projects using the publicly available compilers for SCEst and SCCharts. This recently led to the commercial adoption of the SCChart language in the railway domain. The Blech language, developed at Bosch and now also publicly available, heavily builds on SC principles as well.
Publications
- Denotational fixedpoint semantics for constructive scheduling of synchronous concurrency. Acta Informatica, Special Issue on Combining Compositionality and Concurrency, 52(4):393–442, 2015
Joaquín Aguado, Michael Mendler, Reinhard von Hanxleden, and Insa Fuhrmann
(See online at https://doi.org/10.1007/s00236-015-0238-x) - A novel WCET semantics of synchronous programs. In Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings, pages 195–210, 2016
Michael Mendler, Partha S. Roop, and Bruno Bodin
(See online at https://doi.org/10.1007/978-3-319-44878-7_12) - Time for reactive system modeling: Interactive timing analysis with hotspot highlighting. In Proceedings of the 24th International Conference on Real-Time Networks and Systems, RTNS ’16, pages 289–298, New York, NY, USA, 2016. ACM
Insa Fuhrmann, David Broman, Reinhard von Hanxleden, and Alexander Schulz-Rosengarten
(See online at https://doi.org/10.1145/2997465.2997467) - Compositional timing-aware semantics for synchronous programming. In Franco Fummi, Hiren D. Patel, and Samarjit Chakraborty, editors, 2017 Forum on Specification and Design Languages, FDL 2017, Verona, Italy, September 18-20, 2017, pages 1–8. IEEE, 2017
Joaquín Aguado, Michael Mendler, Jia Jie Wang, Bruno Bodin, and Partha S. Roop
(See online at https://doi.org/10.1109/FDL.2017.8303895) - Real-time ticks for synchronous programming. In Proc. Forum on Specification and Design Languages (FDL ’17), Verona, Italy, September 2017
Reinhard von Hanxleden, Timothy Bourke, and Alain Girault
(See online at https://doi.org/10.1109/FDL.2017.8303893) - SCEst: Sequentially Constructive Esterel. ACM Transactions on Embedded Computing Systems (TECS)—Special Issue on MEMOCODE 2015, 17(2):33:1–33:26, December 2017
Steven Smyth, Christian Motika, Karsten Rathlev, Reinhard von Hanxleden, and Michael Mendler
(See online at https://doi.org/10.1145/3063129) - Timing analysis of synchronous programs using WCRT algebra: Scalability through abstraction. ACM Transactions on Embedded Computing Systems (TECS), 16(5s):177:1–177:19, October 2017
J. Wang, M. Mendler, P. Roop, and B. Bodin
(See online at https://doi.org/10.1145/3126520) - Deterministic concurrency: A clock-synchronised shared memory approach. In 27th European Symposium on Programming, ESOP’18, pages 86–113, Thessaloniki, Greece, April 2018
Joaquín Aguado, Michael Mendler, Marc Pouzet, Partha S. Roop, and Reinhard von Hanxleden
(See online at https://doi.org/10.1007/978-3-319-89884-1_4) - Time in SCCharts. In Tom J. Kazmierski, Sebastian Steinhorst, and Daniel Große, editors, Languages, Design Methods, and Tools for Electronic System Design: Selected Contributions from FDL 2018, pages 1–25. Springer, 2020
lexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, and Julien Deantoni
(See online at https://doi.org/10.1007/978-3-030-31585-6_)
