OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Towards a verified compiler prototype for the synchronous language SIGNAL

Zhibin, Yang and Bodeveix, Jean-Paul and Filali, Mamoun and Hu, Kai and Zhao, Yongwang and Ma, Dianfu Towards a verified compiler prototype for the synchronous language SIGNAL. (2016) Frontiers of Computer Science, vol. 10 (n° 1). pp. 37-53. ISSN 2095-2228

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
1MB

Official URL: http://dx.doi.org/10.1007/s11704-015-4364-y

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.

Item Type:Article
Additional Information:Thanks to Springer Verlag. The definitive version is available at http://link.springer.com The original PDF of the article can be found at Frontiers of Computer Science website : http://link.springer.com/journal/11704
HAL Id:hal-01298793
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Beihang University (CHINA)
Other partners > Nanjing University of Aeronautics and Astronautics – NUAA (CHINA)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:06 Apr 2016 14:11

Repository Staff Only: item control page