期刊文献+

Towards a verified compiler prototype for the synchronous language SIGNAL 被引量:8

Towards a verified compiler prototype for the synchronous language SIGNAL
原文传递
导出
摘要 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 nu- clear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL com- piler, 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 transla- tion from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theo- rem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multi- threaded 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 multi- threaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in archi- tecture analysis and design language (AADL), and map the multi-threaded code to this model. 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 nu- clear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL com- piler, 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 transla- tion from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theo- rem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multi- threaded 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 multi- threaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in archi- tecture analysis and design language (AADL), and map the multi-threaded code to this model.
出处 《Frontiers of Computer Science》 SCIE EI CSCD 2016年第1期37-53,共17页 中国计算机科学前沿(英文版)
关键词 synchronous languages SIGNAL guarded ac-tions verified compiler COQ architecture analysis and designlanguage (AADL) synchronous languages, SIGNAL, guarded ac-tions, verified compiler, Coq, architecture analysis and designlanguage (AADL)
  • 相关文献

参考文献3

二级参考文献85

  • 1Berry G. The foundations of Esterel. In: Proof, Language, and Inter- action. 2000, 425--454. 被引量:1
  • 2Halbwachs N. A synchronous language at work: the story of lustre. In: Proceedings of the 3rd ACM and IEEE International Conference on Formal Methods and Models for Co-Design. 2005, 3-11. 被引量:1
  • 3Gamati A. Designing embedded systems with the Signal program- ming language: synchronous, reactive specification. Springer Pub- fishing Company, Incorporated, 2009. 被引量:1
  • 4Inria. The coq proof assitant, http://coq.inria.fr. 被引量:1
  • 5Do- 178c. http://rtca.org. 被引量:1
  • 6Pnueli A, Siegel M, Singerman E. Translation validation. Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1998, 151-166. 被引量:1
  • 7Pnueli A, Shtrichman O, Siegel M. Translation validation: from Sig- nal to C. Lecture Notes in Computer Science, 1999,1710:231-255. 被引量:1
  • 8Inria. The compcert project, http://compcert.inria.fr. 被引量:1
  • 9Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83-94. 被引量:1
  • 10Tristan J B, Govereau P, Morrisett G. Evaluating value-graph transla- tion validation for LLVM. ACM Sigplan Notices, 2011, 295-305. 被引量:1

共引文献11

同被引文献27

引证文献8

二级引证文献26

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部