Author(s)

F. Defossez, P. Bon & S. Collart-Dutilleul

Abstract

This paper aims at showing how it is possible to combine the advantages of highlevel Petri nets and the B method in order to design safety applications. In the railway critical software domain, safety requirements are obviously severe. Indeed, the passing from an informal specification to a formal one is a crucial point in critical software development. High-level Petri nets combine three important features: a graphical representation, a dynamic behaviour and an abstraction of the treatments. The B method allows one to pass from an abstract specification to a concrete implementation. We propose an approach that integrates the structuring and modelling of the system behaviour by means of coloured Petri nets from semi-formal specifications and the generation of a B abstract specification from this Petri net. Keywords: railway critical systems, safety, formal methods, model translation, high-level Petri nets, B method. 1 Introduction The technological progress of safety automation in railway systems involves a growing complexity of functional safety requirements. Thereby, this leads to the use of some technical tools for analysis and command synthesis that are more and more complex and efficient in order to respect the requirements. Moreover, the introduction of new European standards for railway safety has led one to reconsider critical system requirement specifications modelling.

Keywords

railway critical systems, safety, formal methods, model translation, high-level Petri nets, B method.