Use of formal methods in embedded software development: stakes, constraints and proposal

Anthony Fernandes Pires 1 Thomas Polacsek 1 Virginie Wiels 1 Stéphane Duprat 2
1 ONERA - The French Aerospace Lab [Toulouse]
2 Atos Intégration SAS
Abstract : In aeronautics, software development is submitted to strong constraints. The DO-178 certification standard specifies development and verification objectives. Moreover, its supplement DO-333 defines guidelines for the use of formal methods in this context. Formal methods are used in industry for different purposes and often require the intervention of experts for their processing. In this paper, we propose an approach to answer a certification objective using formal methods while keeping them usable for non-experts. We present an automatic method to check the compliance of a C source code according to its Low Level Requirements expressed as an UML state machine and we show how it addresses objectives of the DO-333.
Keywords : Certification aeronautics formal methods model driven engineering verification and validation
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
https://hal-onera.archives-ouvertes.fr/hal-02272049
Contributor : Axelle Pagnier <>
Submitted on : Tuesday, August 27, 2019 - 2:32:05 PM
Last modification on : Thursday, August 29, 2019 - 1:21:50 AM

File

ERTS_2014_submission_35.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02272049, version 1

Collections

ONERA | ERTS2014

Citation

Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels, Stéphane Duprat. Use of formal methods in embedded software development: stakes, constraints and proposal. Embedded real-time software and systems (ERTS² 2014), Feb 2014, TOULOUSE, France. ⟨hal-02272049⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

4

Files downloads

4

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD