Towards the Formal Analysis of Algorithmic Requirements

Informal requirements are often ambiguous, hence leaving the choice of an interpretation to the implementation phase. In this paper, we describe an experience in the development of a safety-critical software component for on-board train control. Despite the requirements being part of the ERTMS standard, the development resulted in multiple iterations, with increases in cost and delays in delivery. These problems could be traced back to ambiguities of the natural language. As a result, we investigate a formal approach for the analysis of requirements. The idea is to formalize the informal specifications while ensuring traceability, and to encode various forms of validation. The methodology is based on Satisfiability Modulo Theories and encompasses user-defined as well as structural properties.