[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

  • Research Article
  • Published:
Frontiers of Computer Science Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems, 1989, F(13): 477–498

    MathSciNet  MATH  Google Scholar 

  2. Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1–21

    Google Scholar 

  3. Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293–1304

    Article  Google Scholar 

  4. Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 1991, 79(9): 1305–1320

    Article  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  6. Schneider K. The synchronous programming language QUARTZ. Internal Report. Kaiserslautern: University of Kaiserslautern, 2010

    Google Scholar 

  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

    Article  Google Scholar 

  8. Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of International Conference on Concurrency Theory. 1999, 162–177

    Chapter  Google Scholar 

  9. Feautrier P, Gamatié A, Gonnord L. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction. Technical Report. 2013

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  12. Dijkstra E W. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457

    Article  MathSciNet  MATH  Google Scholar 

  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

    Google Scholar 

  14. Brandt J, Schneider K. Separate translation of synchronous programs to guarded actions. Internal Report 382/11, Kaiserslautern: University of Kaiserslautern, 2011

    Google Scholar 

  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

    Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Article  Google Scholar 

  21. RTCA/DO-178B. Software considerations in airborne systems and equipment certification. RTCA Inc., 1992

    Google Scholar 

  22. RTCA/DO-178C. Software considerations in airborne systems and equipment certification. RTCA Inc., 2011

    Google Scholar 

  23. Pouzet M. Lucid Synchrone, version 3: tutorial and reference manual. Université Paris-Sud, LRI, 2016

    Google Scholar 

  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

    Google Scholar 

  25. Castéran P, Bertot Y. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. New York: Springer, 2004

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  28. Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010

    Google Scholar 

  29. Gamatié A. Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification. Springer Science and Business Media, 2009

    Google Scholar 

  30. Le Guernic P, Gautier T. Data-Flow to von Neumann: the SIGNAL approach. Advanced Topics in Data-Flow Computing, 1991, 413–438

    Google Scholar 

  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

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  MathSciNet  Google Scholar 

  36. Amagbegnon T, Besnard L, Le Guernic P. Arborescent canonical form of boolean expressions. Dissertation for the Doctoral Degree. 1994

    Google Scholar 

  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

    Google Scholar 

  38. Leroy X. Mechanized semantics for compiler verification. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 4–6

    Chapter  Google Scholar 

  39. Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115

    Article  Google Scholar 

  40. Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83–94

    Article  Google Scholar 

  41. Necula G C. Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 106–119

    Google Scholar 

  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

    Chapter  Google Scholar 

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

    Google Scholar 

  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

    Article  MathSciNet  Google Scholar 

  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

    Google Scholar 

Download references

Acknowledgements

This work was supported in part by the National Natural Science Foundation of China (Grant No. 61502231), the Natural Science Foundation of Jiangsu Province (BK20150753), the National Defense Basic Scientific Research Project (JCKY2016203B011), the Project of the State Key Laboratory of Software Development Environment of China (SKLSDE-2015KF-04), the Avionics Science Foundation of China (2015ZC52027), China Postdoctoral Science Foundation, and the Open Project of Shanghai Key Laboratory of Trustworthy Computing (07dz22304201502), and the RTRA STAE Foundation in France.

Author information

Authors and Affiliations

  1. School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, 211106, China

    Zhibin Yang

  2. State Key Laboratory of Software Development Environment, Beijing, 100191, China

    Zhibin Yang

  3. Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, 211106, China

    Zhibin Yang

  4. IRIT-CNRS, Université de Toulouse, Toulouse, 31062, France

    Jean-Paul Bodeveix & Mamoun Filali

Authors
  1. Zhibin Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Paul Bodeveix
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mamoun Filali
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Zhibin Yang, Jean-Paul Bodeveix or Mamoun Filali.

Additional information

Zhibin Yang is an associate professor at Nanjing University of Aeronautics and Astronautics, China. He received his PhD degree in computer science from Beihang University, China in 2012. From 2012 to 2014, he was a Postdoc in IRIT of University of Toulouse, France. His research interests include safety-critical real-time system, formal verification, AADL, and synchronous languages.

Jean-Paul Bodeveix received his PhD degree in computer science from the University of Paris-Sud 11, France in 1989. He has been an assistant professor at University of Toulouse III, France since 1989 and is now a professor of computer science since 2003. His main research interests concern formal specifications, automated and assisted verification of protocols as well as of proof environments. He has participated in various European and national projects related to these domains. His current activities are linked to real time modeling and verification either via model checking techniques or at the semantics level.

Mamoun Filali is a full-time researcher at CNRS (Centre National de la Recherche Scientifique), France. His main research interests concern the certified development of embedded systems, formal methods, model checking and theorem proving. During the last years, he has been mainly involved in the french nationwide TOPCASED project where he was concerned by the verification topic. He has also participated in the proposal of the AADL behavioral annex which has been adopted as part of the AADL SAE standard.

Electronic supplementary material

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Yang, Z., Bodeveix, JP. & Filali, M. Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL. Front. Comput. Sci. 13, 715–734 (2019). https://doi.org/10.1007/s11704-017-6485-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11704-017-6485-y

Keywords

Search

Navigation