OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Verified Transformation: From Polychronous Programs to a Variant of Clocked Guarded Actions

Yang, Zhibin and Bodeveix, Jean-Paul and Filali, Mamoun and Kai, Hu and Ma, Dianfu A Verified Transformation: From Polychronous Programs to a Variant of Clocked Guarded Actions. (2014) In: 17th International Workshop on Software and Compilers for Embedded Systems (SCOPES 14), 10 June 2014 - 11 June 2014 (Sankt Goar, Germany).

[img] (Document in English)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
973kB

Official URL: http://dx.doi.org/10.1145/2609248.2609259

Abstract

SIGNAL belongs to the synchronous languages family. Such languages 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 key step of a verified SIGNAL compiler prototype, that is the transformation from a subset of SIGNAL to S-CGA (a variant of clocked guarded actions) and the proof of semantics preservation. Compared with the existing SIGNAL compiler, we use clocked guarded actions as the intermediate representation, to integrate more synchronous programs into our verified compiler prototype in the future. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. Thus, we propose a variant of clocked guarded actions, namely S-CGA, which constrains variable accesses as done by SIGNAL. To conform with the revised semantics of clocked guarded actions, we also do some adjustments on the existing translation rules from SIGNAL to clocked guarded actions. Finally, the verified transformation is mechanized in the theorem prover Coq.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to ACM editor. The definitive version is available at http://dl.acm.org This papers appears in SCOPES '14 Proceedings of the 17th International Workshop on Software and Compilers for Embedded Systems ISBN: 978-1-4503-2941-5 The original PDF is available at: http://dl.acm.org/citation.cfm?doid=2609248.2609259
Audience (conference):International conference proceedings
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)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:18 Jun 2015 08:08

Repository Staff Only: item control page