TY - GEN
T1 - A verified transformation
T2 - 17th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2014
AU - Yang, Zhibin
AU - Bodeveix, Jean Paul
AU - Filali, Mamoun
AU - Hu, Kai
AU - Ma, Dianfu
PY - 2014/6/10
Y1 - 2014/6/10
N2 - SIGNAL belongs to the synchronous languages family. Such languages are widely used in the design of safety-critical realtime 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.
AB - SIGNAL belongs to the synchronous languages family. Such languages are widely used in the design of safety-critical realtime 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.
KW - Guarded actions
KW - SIGNAL
KW - Semantics preservation
KW - Synchronous languages
KW - Verified compiler
UR - https://www.scopus.com/pages/publications/84908885997
U2 - 10.1145/2609248.2609259
DO - 10.1145/2609248.2609259
M3 - 会议稿件
AN - SCOPUS:84908885997
T3 - Proceedings of the 17th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2014
SP - 128
EP - 137
BT - Proceedings of the 17th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2014
A2 - Stuijk, Sander
PB - Association for Computing Machinery
Y2 - 10 June 2014 through 11 June 2014
ER -