Safety critical software construction using CPN modeling and B method's proof
BOUDI ; EL KOURSI ; COLLART-DUTILLEUL
Type de document
COMMUNICATION AVEC ACTES INTERNATIONAL (ACTI)
Langue
anglais
Auteur
BOUDI ; EL KOURSI ; COLLART-DUTILLEUL
Résumé / Abstract
Meeting the strict safety requirements in critical software development is today crucial for the safety-related industrial environment, especially railways. To be able to prove that all safety properties are captured in the system requirements and software specifications, as well as that the final software product satisfies all specifications, a formal approach is the most convenient. Indeed, the use of formal means of description in the development process was highly recommended by the CENELEC standard. Accordingly, this paper presents by means of a level-crossing gate controller case study, the practical use of Colored Petri Nets transformation into B abstract machines for safety critical software development.
