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

Bernard Dion

doi:10.4271/2004-01-1735

2004-03-08

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

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.

SAE MOBILUS

Subscribers can view annotate, and download all of SAE's content. Learn More »

Access SAE MOBILUS »

Digital $37.00 Print $37.00

Preview Document

We also recommend:

Standards

SAE Mobilus®

Publications

News

Events

Professional Development

A World in Motion (PreK-12)

Participate with SAE

SAE Membership

Donate

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

SAE MOBILUS