The Role of Formal Methods in Software Procurement for the Railway Transportation Industry

The present paper reports the experience of a joint project between Politecnico di Milano and Italian State Railway FS, Infrastructure Department( became Rete Ferroviaria Italiana S.p.A.: R.F.I. S.p.A.). The purpose of the project was to define procedures and rules for managing software procurement for safety-critical signalling equipment. The project covers all phases of system development, from requirements elicitation to implementation and final validation, providing requirements on methods, languages and tools to be used during software development, without any bias towards any particular technology or tool provider. The results are consistent with, and acceptable against, international standards. In particular, Requirements/Recommendations have been issued, tailored on various kinds of systems under examination, concerning: a) methods, techniques, languages and tools; b) organization of the provider company in terms of independence and responsibility of participating actors; c) documentation to be produced by the provider. A first experimental evaluation of formal specification methods applied to signalling systems is also reported, and we outline a further experimentation, where the results presented here will be applied on an industrial scale in the procurement, by RFI, of a complex signaling apparatus.