Taking advantage of some complementary modelling methods to meet critical system requirement specifications

摘要

This paper aims at showing how it is possible to combine the advantages of high-level 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.