research-article

Experience report: using objective caml to develop safety-critical embedded tools in a certification framework

Authors:

Jean-Louis ColaçoAuthors Info & Claims

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

Pages 215 - 220

https://doi.org/10.1145/1596550.1596582

Published: 31 August 2009 Publication History

Get Access

Abstract

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE SUITE 6TM certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO-178B, IEC 61508, EN 50128 and such.

Supplementary Material

JPG File (experiencereportusingobjectivecamltodevelopsafety-critical.jpg)

Download
20.77 KB

MP4 File (experiencereportusingobjectivecamltodevelopsafety-critical.mp4)

Download
118.00 MB

References

[1]

Gérard Berry. The Effectiveness of Synchronous Languages for the Development of Safety-Critical Systems. Technical report, Esterel-Technologies, 2003.

Google Scholar

[2]

Jean-Louis Camus and Bernard Dion. Efficient Development of Airborne Software with SCADE Suite TM. Technical report, Esterel-Technologies, 2003.

Google Scholar

[3]

Jean-Louis Colaço and Marc Pouzet. Clocks as First Class Abstract Types. In Third International Conference on Embedded Software (EMSOFT'03), Philadelphia, Pennsylvania, USA, oct 2003.

Crossref

Google Scholar

[4]

Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, sep 2005.

Digital Library

Google Scholar

[5]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The astrée analyser. In European Symposium on Programming. LNCS, April 2005.

Google Scholar

[6]

ECMA-367: Eiffel analysis, design and programming language. ECMA (European Association for Standardizing Information and Communication Systems), pub-ECMA:adr, June 2005.

Google Scholar

[7]

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. In Proceedings of the IEEE, pages 1305--1320, 1991.

Crossref

Google Scholar

[8]

Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson. A Practical Tutorial on Modified Condition/Decision Coverage. Technical report, NASA/TM-2001-210876, May 2001.

Google Scholar

[9]

Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, documentation and user's manual - release 3.11. INRIA, December 2008. URL http://caml.inria.fr/pub/docs/manual-ocaml/.

Google Scholar

[10]

Bruno Pagano, Olivier Andrieu, Benjamin Canou, Emmanuel Chailloux, Jean-Louis Colaço, Thomas Moniot, and Philippe Wang. Certified development tools implementation in objective caml. In Paul Hudak and David Scott Warren, editors, Tenth International Symposium on Practical Aspects of Declarative Languages (PADL), volume 4902 of Lecture Notes in Computer Science, pages 2--17. Springer, 2008.

Digital Library

Google Scholar

[11]

Marc Pouzet. Lucid Synchrone version 3.0 : Tutorial and Reference Manual, 2006. (www.lri.fr/%7Epouzet/lucid-synchrone).

Google Scholar

[12]

The Coq Development Team LogiCal Project. The Coq Proof Assistant Reference Manual, 2006. (coq.inria.fr/V8.1beta/refman).

Google Scholar

[13]

RTCA/DO-178B. Software Considerations in Airborne Systems and Equipment Certification. Radio Technical Commission for Aeronautics RTCA, pages 31,74, December 1992.

Google Scholar

Cited By

View all

PEREZ IGOODLOE A(2020)Fault-tolerant functional reactive programming (extended version)Journal of Functional Programming10.1017/S095679682000011830Online publication date: 7-May-2020
https://doi.org/10.1017/S0956796820000118
Wang PJonquet AChailloux E(2019)Non-Intrusive Structural Coverage for Objective CamlElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2011.02.006264:4(59-73)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/j.entcs.2011.02.006
Yang ZBodeveix JFilali M(2019)Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNALFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-017-6485-y13:4(715-734)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1007/s11704-017-6485-y
Show More Cited By

Index Terms

Experience report: using objective caml to develop safety-critical embedded tools in a certification framework
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
    2. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

Experience report: using objective caml to develop safety-critical embedded tools in a certification framework
ICFP '09

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and ...
Safety critical Java™ technology
JTRES '06: Proceedings of the 4th international workshop on Java technologies for real-time and embedded systems

A specification for Java in safety critical systems is being developed by The Open Group under the Java Community Process. The JSR-302 Expert Group has begun work to create this specification based on the Real-Time Specification for Java (RTSJ) that ...
Position paper: DO-178C/ED-12C and object-orientation for critical systems
Ada-Europe'11: Proceedings of the 16th Ada-Europe international conference on Reliable software technologies

DO-178C/ED-12C, six years in preparation, is expected to be published in 2011. This updated document will provide guidance for the development and verification of safety-related software for avionic systems. As this position paper will describe, DO-178C/...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

August 2009

364 pages

ISBN:9781605583327

DOI:10.1145/1596550

General Chair:
Graham Hutton
University of Nottingham
,
Program Chair:
Andrew Tolmach
Portland State University

ACM SIGPLAN Notices Volume 44, Issue 9
ICFP '09
September 2009
343 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1631687
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '09

Sponsor:

ICFP '09: ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2009

Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
465
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)2

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

PEREZ IGOODLOE A(2020)Fault-tolerant functional reactive programming (extended version)Journal of Functional Programming10.1017/S095679682000011830Online publication date: 7-May-2020
https://doi.org/10.1017/S0956796820000118
Wang PJonquet AChailloux E(2019)Non-Intrusive Structural Coverage for Objective CamlElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2011.02.006264:4(59-73)Online publication date: 5-Jan-2019
https://dl.acm.org/doi/10.1016/j.entcs.2011.02.006
Yang ZBodeveix JFilali M(2019)Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNALFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-017-6485-y13:4(715-734)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1007/s11704-017-6485-y
Perez I(2018)Fault tolerant functional reactive programming (functional pearl)Proceedings of the ACM on Programming Languages10.1145/32367912:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236791
Colaco JPagano BPasteur CPouzet M(2018)Scade 6: From a Kahn Semantics to a Kahn Implementation for Multicore2018 Forum on Specification & Design Languages (FDL)10.1109/FDL.2018.8524052(5-16)Online publication date: Sep-2018
https://doi.org/10.1109/FDL.2018.8524052
Davy GGarion CGaroche PRoux PThirioux X(2018)Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code2018 Forum on Specification & Design Languages (FDL)10.1109/FDL.2018.8524044(5-16)Online publication date: Sep-2018
https://doi.org/10.1109/FDL.2018.8524044
Colaco JPagano BPouzet M(2017)SCADE 6: A formal language for embedded critical software development (invited paper)2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2017.8285623(1-11)Online publication date: Sep-2017
https://doi.org/10.1109/TASE.2017.8285623
Vaugon BWang PChailloux E(2015)Programming Microcontrollers in OCaml: The OCaPIC ProjectPractical Aspects of Declarative Languages10.1007/978-3-319-19686-2_10(132-148)Online publication date: 14-May-2015
https://doi.org/10.1007/978-3-319-19686-2_10
Pike LWegmann NNiller SGoodloe A(2012)Experience reportACM SIGPLAN Notices10.1145/2398856.236455347:9(335-340)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364553
Pike LWegmann NNiller SGoodloe AThiemann PFindler R(2012)Experience reportProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364553(335-340)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364553
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Experience report: using objective caml to develop safety-critical embedded tools in a certification framework

Safety critical Java™ technology

Position paper: DO-178C/ED-12C and object-orientation for critical systems