Synchronous data-flow languages (SDFL), such as Lustre , is a concurrent language that has been widely used in safety-critical systems. Verified compilers for such languages are crucial in generating trustworthy object code. A good approach is to first translate a concurrent SDFL program to a sequential intermediate representation, such as a Clight  code, and then use an existing verified compiler such as CompCert  to produce executable object code for the target machine. A verified Sequentializer is crucial in such a verified compiler. It produces a sequential topological order among the program statements that preserve the program dependencies and the dynamic semantics of the original program. In this paper, we show such an approach for a SDFL language such as Lustre. The approach is general enough to be applicable to other SDFLs as well. It first gives a formal specification of the operational semantics, and proves its determinism property for a Lustre-like program. It then formally proves the equivalence of the original concurrent semantics and its target sequential semantics using the well-established proof assistant Coq (, ), and extracts the certified code for such a sequentializer by Coq.
|Original language||English (US)|
|Title of host publication||Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||3|
|State||Published - Jun 30 2017|
|Event||39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017 - Buenos Aires, Argentina|
Duration: May 20 2017 → May 28 2017
|Name||Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017|
|Other||39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017|
|Period||5/20/17 → 5/28/17|
Bibliographical noteFunding Information:
The work was supported in part by NSFC (Grant No.61462086), MIIT (Grant No.MJ-2015-D-066) and LIAMA (grants for the project FCST).
- Synchronous Data-flow Languages
- Verified Compiler