Information Technology Reference
In-Depth Information
Formal Specification and Automated
Verification
of Safety-Critical Requirements of a Railway
Vehicle with Frama-C/Jessie
Kerstin Hartig
1
, Jens Gerlach
1
,JuanSoto
1
, and Jürgen Busse
2
1
Fraunhofer FIRST, Berlin, Germany
{kerstin.hartig, jens.gerlach, juan.soto}@first.fraunhofer.de
2
Institute of Railway Technology, IfB GmbH, Berlin, Germany
jb@bahntechnik.de
Abstract. Formal verification of software provides a higher level of
assurance than classical software testing. In this paper, we report on
our experience with the Frama-C/Jessie verification tool in the rail-
way domain. We analyse safety-critical requirements of a railway ve-
hicle, formalize them using the ANSI/ISO-C Specification Language
(ACSL) and achieve automated proofs to verify that the implemen-
tation satisfies the formal specification. The main requirement for
the successful application of Frama-C in the railway domain is its
qualification according to EN 50128.
Keywords: Frama-C/Jessie, ACSL, Unit Proof, EN 50128, Railway Do-
main
1
Introduction
Developers of industrial critical embedded software face numerous challenges.
They must ensure their software provides high levels of assurance, often,
within tight time constraints. In addition, they generally have limited bud-
gets for conducting software testing. However, regardless of how much soft-
ware testing is performed, one cannot fully guarantee that a safety feature is
satisfied. Hence, one must resort to the use of formal methods. Notwithstand-
ing, it is the assessor and the certification authority that must be convinced
that software meets the safety-critical requirements contained within stan-
dards, such as the EN 50128 standard for railway software.
Our work addresses the promotion and adoption by industry of a partic-
ular formal method, namely, deductive verification, based on an open source
tool, called Frama-C within the framework of the DEVICE-SOFT
3
project.
3
DEVICE-SOFT stands for Deductive Verification of Industrial Critical Embed-
ded Software.
