Validation and Verification of the safety Kernel of the Naples subway

We report on an experience in the application of formal methods to the specification, validation and verification of a railway signaling system: the safety kernel of the Naples Subway. The activity was performed ex post, several years after final system delivery, based on the design documentation [4, 1]. We first illustrate the requirement specification using the object-oriented temporal logic TRIO. Then we relate on the use of the specification, by means of suitable support tools, to validate the requirements and to generate some scenarios to be employed as test cases in the verification phase.