Formal Validation & Verification of Software for Railway Control and Protection Systems: Experimental Applications in ANSALDO

The ever increasing use of software-based controllers provides flexible and complex functions at a reasonable cost, extremely lower than traditional circuitry. However, it poses crucial problems of safety: even though existing software engineering techniques provide structured methodologies for design, implementation, testing, verification and validation of software, safety in software systems is harder to demonstrate than in traditional relays circuitry. An approach to safety assurance which can provide significant help is the use of `Formal Validation & Verification` (Formal V&V). The idea is to use a mathematical model for software specification, design and implementation, and mathematical algorithm for the validation and verification of such a model. In this paper we report on the experimentation with Formal V&V carried out in ANSALDO. We have devised the possibility of integrating the technology within the traditional development process, and have estimated the costs and benefits of such introduction. After an assessment of the state of the art, Model Checking has been identified as a particularly promising technique for Formal V&V, for its ability to perform validations in fully automated way and pinpoint anomalous behaviours at early stages of the design cycle. Experiments have been carried out on a case study taken from one of ANSALDO safety critical applications