Correct-By-Construction Methods for the Development of Safety-Critical Applications

2004-01-1735

03/08/2004

Event
SAE 2004 World Congress & Exhibition
Authors Abstract
Content
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.
Meta TagsDetails
DOI
https://doi.org/10.4271/2004-01-1735
Pages
10
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.
Additional Details
Publisher
Published
Mar 8, 2004
Product Code
2004-01-1735
Content Type
Technical Paper
Language
English