Skip to Main content Skip to Navigation
Journal articles

Towards a verified compiler prototype for the synchronous language SIGNAL

Abstract : SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL compiler, we propose a new intermediate representation (named S-CGA, a variant of clocked guarded actions), to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the translation from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theorem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multithreaded code generation with time-predictable properties. With the rising importance of multi-core processors in safety-critical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multithreaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in architecture analysis and design language (AADL), and map the multi-threaded code to this model.
Complete list of metadatas

Cited literature [40 references]  Display  Hide  Download
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Wednesday, April 6, 2016 - 4:12:00 PM
Last modification on : Thursday, June 11, 2020 - 4:49:45 AM
Long-term archiving on: : Monday, November 14, 2016 - 5:59:53 PM


Files produced by the author(s)



Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu, Yongwang Zhao, et al.. Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers of Computer Science, Springer Verlag, 2016, vol. 10 (n° 1), pp. 37-53. ⟨10.1007/s11704-015-4364-y⟩. ⟨hal-01298793⟩



Record views


Files downloads