Case study: Formal verification of a computerized railway interlocking
type: Item
instance of: scholarly article
title: Case study: Formal verification of a computerized railway interlocking
zbMATH Open document ID: 1111.68499
author: Arne Borälv
published in: Formal Aspects of Computing
publication date: 1999-07-26T00:00:00Z
review text: We describe a case study in system-level verification of a computerized railway interlocking developed by ADtranz Spain, installed and put into test use at a subway station in Madrid. The formal modelling and analysis was carried out by personell at ADtranz Sweden using a tool for automatic formal modelling of the interlocking system and the commerical verification software NP-Tools, which is based on Stålmarck's patented proof procedure. The case study took about one man week in total, of which most of the time was spent modelling safety requirements. The analysis discovered an error that had passed the traditional verification phase. The actual analysis time, disproving the safety requirements by supplying a countermodel, was done in a matter of seconds. The corrected software could be proved to fulfil the safety requirements in the same amount of time. This case study is one of many carried out by ADtranz during 1995--98 in the process in which they have replaced the traditional techniques used for system level verification of safety with formal techniques. We give an overview of the formal methods and tools used which today are integrated in the development environment at ADtranz.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 1309026
MaRDI profile type: Publication
full work available at URL: s001650050021
OpenAlex ID: W2007808472
DOI: 10.1007/S001650050021
description: scientific article; zbMATH DE number 1309026