The Role of Formal Methods in Software Development for Railway Applications

The Role of Formal Methods in Software Development for Railway Applications

Alessandro Fantechi (Università degli Studi di Firenze, Italy)
DOI: 10.4018/978-1-4666-1643-1.ch012
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.
Chapter Preview
Top

Background

Early Applications of Formal Methods

Nowadays, the necessity of formal methods as an essential step in the design process of industrial safety-critical systems is widely recognized.

In its more general definition, the term formal methods encompasses all notations having a precise mathematical semantics, together with their associated analysis and development methods, that allow to describe and reason about the behaviour and functionality of a system in a formal manner, with the aim to produce an implementation of the system that is provably free from defects.

Railway signaling has been traditionally considered as one of the most fruitful areas of intervention for formal methods (Fantechi, Fokkink, & Morzenti, 2011). Already in the early nineties, a series of railway signaling products have benefited from the application of the B formal method in the design process.

The B method (Abrial, 1996) targets software development from specification through refinement, down to implementation and automatic code generation, with formal verification at each refinement step: writing and refining a specification produces a series of proof obligations that need to be discharged by formal proofs. The B method is accompanied by support tools, which include tools for the derivation of proof obligations, theorem provers, and code generation tools.

The B method has been successfully applied to several railway signalingsignaling systems. The SACEM system for the control of a line of Paris RER (DaSilva, Dehbonei, & Mejia, 1993) is the first acclaimed industrial application of B. B has been adopted for many later designs of similar systems by Matra (now absorbed by Siemens). One of the most striking application has been the Paris automatic metro line 14. The paper (Behm, Benoit, Faivre, & Meynadier, 1999) on this application of B reports that several errors were found and corrected during proof activities conducted at the specification and refinement stages. By contrast, no further bugs were detected by the various testing activities that followed the B development.

Complete Chapter List

Search this Book:
Reset