Information Technology Reference
In-Depth Information
Frama-C is a suite of tools dedicated to the analysis of the source code of soft-
ware written in C. Frama-C is particularly interesting for us because C is an
important programming language for the development of safety-critical em-
bedded systems. The development of Frama-C is coordinated by CEA LIST[1]
in Saclay, France. The Frama-C platform is extensible, meaning users can
incorporate new plug-ins. Jessie[2] is a plug-in which enables deductive ver-
ification of C programs within Frama-C. It is based on the computation of
weakest preconditions. Given an ACSL[3] annotated C program, the Jessie
plug-in generates intermediate code and verification conditions for use by
automated theorem provers or interactive proof assistants.
Airbus has successfully used Caveat (a predecessor of Frama-C/Jessie) to
replace unit tests by by unit proofs in parts of their software[4]. With a vast
array of specialty domains to choose from, we opted to focus on the railway
industry, given the fact that it is one of the domains with a vested interest
in the usage of formal methods[5]. Another aspect of the DEVICE-SOFT
project is the development of a deductively verified C-library of standard
algorithms[6].
The particular safety requirements for the vigilance device of a generic
diesel locomotive (see Section 2) were drawn from an experienced assessor
in the evaluation of railway software. Starting from these requirements we
follow the simplified V-model depicted in Figure 1.
Subsystem
Requirements
Analysis
Subsystem
Integration
Subsystem Design and
Formal Specification
Unit Proofs
Implementation
Fig. 1. Formal Subsystem Development Process.
Initially, we analyse the informal requirements of the vigilance device (see
Section 2). We formalize these requirements using the ANSI/ISO C Specifica-
tion Language (see Section 3). Thereby we discuss some of the most important
features of ACSL. In Section 4, we will illustrate some important aspects that
have to be considered when implementing the ACSL specification. Section 5
shows the results of the automated unit proofs that show that the implemen-
tation satisfies its ACSL specification. Finally, we discuss the benefits and
challenges and the qualification of the software tools.
