An Introduction to Formal Methods for the Development of Safety-critical Applications

This report is a delivery to The Danish Government’s railway authority, Trafikstyrelsen, as a part of the Public Sector Consultancy service offered by the Technical University of Denmark. The purpose of the report is to give the reader an insight into the stateof-the-art of formal methods. The reader is assumed to have some knowledge about software development, but not on formal methods.

The background for the railway authorities’ interest in formal methods is the fact that during the next decade a total renewal of the Danish signalling infrastructure is going to take place. Central parts of the new systems will be software components that must fulfill strong safety requirements: in order to get the software certified at the highest Safety Integrity Levels of the European CENELEC standards for railway applications, the software providers are expected to use formal methods.