Taking advantage of some complementary modelling methods to meet critical system requirement specifications
DEFOSSEZ ; BON ; COLLART-DUTILLEUL
Type de document
CHAPITRE D'OUVRAGE (CO)
Langue
anglais
Auteur
DEFOSSEZ ; BON ; COLLART-DUTILLEUL
Résumé / Abstract
This paper aims at showing how it is possible to combine the advantages of high-level Petri nets and of 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 the 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 to pass from an abstract specification to a concrete implementation. We propose an approach that integrates the structuting and the 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.
Editeur
Wit Press
