Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL
Pages 715 - 734
Abstract
This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.
References
[1]
Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems, 1989, F(13): 477---498
[2]
Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1---21
[3]
Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293---1304
[4]
Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 1991, 79(9): 1305---1320
[5]
Benveniste A, Le Guernic P, Jacquemot C. Synchronous programming with events and relations: the SIGNAL language and its semantics. Science of Computer Programming, 1991, 16(2): 103---149
[6]
Schneider K. The synchronous programming language QUARTZ. Internal Report. Kaiserslautern: University of Kaiserslautern, 2010
[7]
Teehan P, Greenstreet M, Lemieux G. A survey and taxonomy of GALS design styles. IEEE Design and Test of Computers, 2007, 24(5): 418---428
[8]
Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of International Conference on Concurrency Theory. 1999, 162---177
[9]
Feautrier P, Gamatié A, Gonnord L. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction. Technical Report. 2013
[10]
Gamatié A, Gautier T, Le Guernic P. Towards static analysis of SIGNAL programs using interval techniques. In: Proceedings of Synchronous Languages, Applications, and Programming. 2006
[11]
Gamatié A, Gautier T, Besnard L. An interval-based solution for static analysis in the SIGNAL language. In: Proceedings of the 15th Annual IEEE International Conference andWorkshop on Engineering of Computer Based Systems. 2008, 182---190
[12]
Dijkstra E W. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453---457
[13]
Brandt J, Gemunde M, Shukla S K, Talpin J P. Integrating system descriptions by clocked guarded actions. In: Proceedings of Forum on Specification and Design Languages. 2011, 1---8
[14]
Brandt J, Schneider K. Separate translation of synchronous programs to guarded actions. Internal Report 382/11, Kaiserslautern: University of Kaiserslautern, 2011
[15]
Brandt J, Schneider K, Shukla S K. Translating concurrent action oriented specifications to synchronous guarded actions. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. 2010, 47---56
[16]
Edwards S A, Tardieu O. SHIM: a deterministic model for heterogeneous embedded systems. IEEE Transactions on Very Large Scale Integration Systems, 2006, 14(8): 854---867
[17]
Brandt J, Gemunde M, Schneider K, Shukla A K, Talpin J P. Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, 2014, 18: 63---97
[18]
ESPRIT project: safety critical embedded systems SACRES. The declarative code DC+, version 1.4. Technical Report, 1997
[19]
Yang Z B, Bodeveix J P, Filali M, Hu K, Ma D F. A verified transformation: from polychronous programs to a variant of clocked guarded actions. In: Proceedings of the 17th ACM International Workshop on Software and Compilers for Embedded Systems. 2014, 128---137
[20]
Yang Z B, Bodeveix J P, Filali M, Hu K, Zhao Y W, Ma D F. Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers of Computer Science, 2016, 10(1): 37---53
[21]
RTCA/DO-178B. Software considerations in airborne systems and equipment certification. RTCA Inc., 1992
[22]
RTCA/DO-178C. Software considerations in airborne systems and equipment certification. RTCA Inc., 2011
[23]
Pouzet M. Lucid Synchrone, version 3: tutorial and reference manual. Université Paris-Sud, LRI, 2016
[24]
Forget J. A synchronous language for critical embedded systems with multiple real-time constraints. Dissertation for the Doctoral Degree. Toulouse: Université de Toulouse, 2009
[25]
Castéran P, Bertot Y. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. New York: Springer, 2004
[26]
Pagano B, Andrieu O, Moniot T, Canou B, Chailloux E, Wang P, Manoury P, Colaço J L. Using objective Caml to develop safety-critical embedded tools in a certification framework. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, 2009, 215---220
[27]
Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. The ASTRÉE analyzer. In: Proceedings of the 14th European Symposium on Programming. 2005: 21---30
[28]
Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010
[29]
Gamatié A. Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification. Springer Science and Business Media, 2009
[30]
Le Guernic P, Gautier T. Data-Flow to von Neumann: the SIGNAL approach. Advanced Topics in Data-Flow Computing, 1991, 413---438
[31]
Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(03): 261---303
[32]
Pnueli A, Siegel M, Singerman E. Translation validation. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1998, 151---166
[33]
Talpin J P, Brandt J, Gemunde M, Schneider K, Shukla S K. Constructive polychronous systems. In: Proceedings of International Symposium on Logical Foundations of Computer Science. 2013, 335---349
[34]
Brandt J, Gemunde M, Schneider K, Shukla S K, Talpin J P. Embedding polychrony into synchrony. IEEE Transactions on Software Engineering, 2013, 39(7): 917---929
[35]
Yang Z B, Bodeveix J P, Filali M. A comparative study of two formal semantics of the SIGNAL language. Frontiers of Computer Science, 2013, 7(5): 673---693
[36]
Amagbegnon T, Besnard L, Le Guernic P. Arborescent canonical form of boolean expressions. Dissertation for the Doctoral Degree. 1994
[37]
Jose B A, Gamatié A, Ouy J, Shukla S K. SMT based false causal loop detection during code synthesis from polychronous specifications. In: Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). 2011, 109---118
[38]
Leroy X. Mechanized semantics for compiler verification. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 4---6
[39]
Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107---115
[40]
Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83---94
[41]
Necula G C. Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 106---119
[42]
Chen K, Sztipanovits J, Abdelwalhed S, Jackson E. Semantic anchoring with model transformations. In: Proceedings of European Conference on Model Driven Architecture-Foundations and Applications. 2005, 115---129
[43]
Narayanan A, Karsai G. Using semantic anchoring to verify behavior preservation in graph transformations. Electronic Communications of the EASST, 2006, 4
[44]
Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of synchronous data-flow program transformations toward certified compilers. Frontiers of Computer Science, 2013, 7(5): 598---616
[45]
Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. In: Proceedings of International Conference on Integrated Formal Methods. 2012, 113---127
- Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL
Recommendations
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 nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the ...
Aspectual Caml: an aspect-oriented functional language
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingWe propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. This paper describes the design and implementation ...
Combinators and type-driven transformers in Objective Caml
We describe an implementation of LDTA 2011 Tool Challenge tasks in Objective Caml language. Instead of using some dedicated domain-specific tools we utilize typical functional programming machinery such as polymorphic functions, monads and combinators; ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2019 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 August 2019
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 15 Jan 2025