D. Harel and A. Pnueli, On the development of reactive systems. Logics and Models of Concurrent Systems, pp.477-498, 1989.

P. Castéran and Y. Bertot, Interactive theorem proving and program development: Coq'Art: The Calculus of inductive constructions, 2004.

D. Potop-butucaru, D. Simone, R. Talpin, and J. , The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, pp.1-21, 2005.

F. Boussinot, D. Simone, and R. , The Esterel language, Proceedings of the IEEE, vol.79, pp.1293-1304, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075075

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language Lustre, Proceedings of the IEEE, vol.79, pp.1305-1320, 1991.

A. Benveniste, L. Guernic, P. Jacquemot, and C. , Synchronous programming with events and relations: the Signal language and its semantics. Science of Computer Programming, vol.16, pp.103-149, 1991.

K. Schneider, The synchronous programming language QUARTZ. Internal report, 2010.

P. Teehan, M. Greenstreet, and G. Lemieux, A Survey and Taxonomy of GALS Design Styles, IEEE Design and Test of Computers, vol.24, issue.5, pp.418-428, 2007.

A. Benveniste, B. Caillaud, L. Guernic, and P. , From synchrony to asynchrony, Proceedings of International Conference on Concurrency Theory, pp.162-177, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00073032

P. Feautrier, A. Gamatié, and L. Gonnord, Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00860785

A. Gamatié, T. Gautier, L. Guernic, and P. , Towards Static Analysis of SIG-NAL Programs using Interval Techniques, Proceedings of Synchronous Languages, Applications, and Programming, 2006.

A. Gamatié, T. Gautier, and L. Besnard, An Interval-Based Solution for Static Analysis in the SIGNAL Language, pp.182-190, 2008.

E. Dijkstra, Guarded Commands, Nondeterminacy and Formal Derivation of Programs, Communications of The ACM, vol.18, issue.8, pp.453-457, 1975.

J. Brandt, M. Gemunde, S. Shukla, and J. Talpin, Integrating system descriptions by clocked guarded actions, Proceedings of Forum on Specification and Design Languages, pp.1-8, 2011.

J. Brandt and K. Schneider, Separate translation of synchronous programs to guarded actions, 2011.

J. Brandt, K. Schneider, and S. K. Shukla, Translating concurrent action oriented specifications to synchronous guarded actions, Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, pp.47-56, 2010.

S. Edwards and O. Tardieu, SHIM: a deterministic model for heterogeneous embedded systems, IEEE Transactions on Very Large Scale In

, Foundation, and the Open Project of Shanghai Key Laboratory of Trustworthy Computing under Grant 07dz22304201502, and the RTRA STAE Fountegration Systems, vol.14, pp.854-867, 2006.

J. Brandt, M. Gemunde, K. Schneider, A. Shukla, and J. P. Talpin, Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, vol.18, pp.63-97, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00763334

, Esprit project: Safety Critical Embedded Systems SACRES. The declarative code DC+, vol.IRISA, 1997.

Z. Yang, J. Bodeveix, M. Filali, K. Hu, and D. Ma, A verified transformation: from polychronous programs to a variant of clocked guarded actions, Proceedings of the 17th International Workshop on Software and Compilers for Embedded Systems, pp.128-137, 2014.

Z. Yang, J. Bodeveix, M. Filali, K. Hu, Y. Zhao et al., Towards a verified compiler prototype for the synchronous language SIGNAL, Frontiers of Computer Science, vol.10, issue.1, pp.37-53, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01298793

, RTCA/DO-178B Software Considerations in Airborne Systems and Equipment Certification, 1992.

, RTCA/DO-178C Software Considerations in Airborne Systems and Equipment Certification, 2011.

M. Pouzet, Lucid Synchrone, version 3. Tutorial and reference manual, 2016.

J. Forget, A synchronous language for critical embedded systems with multiple real-time constraints, 2009.
URL : https://hal.archives-ouvertes.fr/tel-01942421

B. Pagano, O. Andrieu, T. Moniot, B. Canou, E. Chailloux et al., Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework, Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, pp.215-220, 2009.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉE analyzer, Proceedings of the 14th European Symposium on Programming, vol.3444, pp.21-30, 2005.

L. Besnard, T. Gautier, L. Guernic, P. Signal-v4-reference, and . Manual, , 2010.

A. Gamatié, Designing embedded systems with the Signal programming language: synchronous, reactive specification, 2009.

L. Guernic, P. Gautier, and T. , Data-Flow to von Neumann: the Signal approach, Advanced Topics in Data-Flow Computing, pp.413-438, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075329

L. Guernic, P. Talpin, J. , and L. Lann, Polychrony for system design, Systems, and Computers, vol.12, issue.03, pp.261-303, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00071871

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.151-166, 1998.

J. Talpin, J. Brandt, M. Gemunde, K. Schneider, and S. K. Shukla, Constructive polychronous systems, Proceedings of International Symposium on Logical Foundations of Computer Science, pp.335-349, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00763371

J. Brandt, M. Gemunde, K. Schneider, S. Shukla, and J. Talpin, Embedding polychrony into synchrony, IEEE Transactions on Software Engineering, vol.39, issue.7, pp.917-929, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00763317

Z. Yang, J. Bodeveix, and M. Filali, A comparative study of two formal semantics of the SIGNAL language, Frontiers of Computer Science, vol.7, issue.5, pp.673-693, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01154264

T. Amagbegnon, L. Besnard, L. Guernic, and P. , Arborescent canonical form of boolean expressions. Irisa, 1994.
URL : https://hal.archives-ouvertes.fr/inria-00074382

B. Jose, A. Gamatié, J. Ouy, and S. K. Shukla, SMT based false causal loop detection during code synthesis from polychronous specifications, Proceedings of 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp.109-118, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00637574

X. Leroy, Mechanized semantics for compiler verification, Proceedings of International Conference on Certified Programs and Proofs, vol.2012, pp.4-6
URL : https://hal.archives-ouvertes.fr/hal-01079337

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

G. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN notices. ACM, vol.35, issue.5, pp.83-94, 2000.

G. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.106-119, 1997.

K. Chen, J. Sztipanovits, S. Abdelwalhed, and J. E. , Semantic anchoring with model transformations, Proceedings of European Conference on Model Driven Architecture-Foundations and Applications, pp.115-129, 2005.

A. Narayanan and G. Karsai, Using semantic anchoring to verify behavior preservation in graph transformations, Electronic Communications of the EASST, p.4, 2006.

J. Talpin, T. Gautier, L. Guernic, P. Besnard, and L. , Formal verification of synchronous data-flow program transformations toward certified compilers, Frontiers of Computer Science, vol.7, issue.5, pp.598-616, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00846279

J. Talpin, T. Gautier, L. Guernic, P. Besnard, and L. , Formal verification of compiler transformations on polychronous equations, Proceedings of International Conference on Integrated Formal Methods. 2012, pp.113-127
URL : https://hal.archives-ouvertes.fr/hal-00730393

. Dr, Zhibin YANG is an associate pro-fessor at Nanjing University of Aero-nautics and Astronautics, China. He received his PhD degree in Computer Science from Beihang University, Bei-jing, 2012.

F. Toulouse, His research interests include safety-critical realtime system, formal verification, AADL, and synchronous languages

. Dr and B. Jean-paul,