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

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