This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Correct-By-Construction Methods for the Development of Safety-Critical Applications
Technical Paper
2004-01-1735
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
In this paper, we will describe how synchronous methods form the scientific basis for the creation of a correct-by-construction methodology required for safety-critical embedded systems. We will show how they are applied to software design, validation, and implementation through a process of high-level rigorous specifications, from which we can create correct-by-construction embeddable implementation.
The synchronous methods we know today have more than 20 years of scientific research plus ten years of successful industrial application. This paper will explore the basic conceptual model of embedded computation supported by three underlying prerequisites: high-level rigorous graphical and textual languages, compiling algorithms for correct-by-construction implementation, and formal testing and verification techniques.
Lastly, we will show how a specialized specification to C compiler automated methodology can create embeddable C code that is automatically correct and certifiable to avionics guidelines DO-178B Level A and that makes low-level testing of generated C code unnecessary. Functional testing can be done at graphical specification level and the generated embeddable C code is automatically correct and certifiable.
Recommended Content
Authors
Topic
Citation
Dion, B., "Correct-By-Construction Methods for the Development of Safety-Critical Applications," SAE Technical Paper 2004-01-1735, 2004, https://doi.org/10.4271/2004-01-1735.Also In
CAE Methods for Vehicle Crashworthiness and Occupant Safety, and Safety-Critical Systems
Number: SP-1870; Published: 2004-03-08
Number: SP-1870; Published: 2004-03-08
SAE 2004 Transactions Journal of Passenger Cars: Electronic and Electrical Systems
Number: V113-7; Published: 2005-07-05
Number: V113-7; Published: 2005-07-05
References
- André C. Representation and Analysis of Reactive Behaviors: A Synchronous Approach proc. CESA'96, IEEE-SMC Lille, France 1996
- Berry G. The Foundations of Esterel “Proofs, Languages, and Interaction, Essays in Honour of Robin Milner” Plotkin G. Stirling C. Tofte M. MIT Press 2000
- Berry G. The Constructive Semantics of Pure Esterel www.estereltechnologies.com
- Edwards S. Languages for Digital Embedded Systems Kluwer Boston, Mass 2000
- Halbwachs N. Synchronous Programming of Reactive Systems Kluwer 1993
- Harel D. Statecharts: a Visual Approach to Complex Systems Science of Computer Programming 8 231 274 1987
- ARP 4754: Certification considerations for highly integrated or complex aircraft systems Society of Automotive Engineers 1996
- DO-178B: Software Considerations in Airborne Systems and Equipment Certification RTCA 1992
- Camus J.L. Dion B. Efficient Development of Airborne Software with SCADE Suite Esterel Technologies www.esterel-technologies.com 2003