Formal Specification and Automated Verification of Railway Software with Frama-C
Résumé
—This paper presents the use of the Frama-C toolkit for the formal verification of a model of train-controlling software against the requirements of the CENELEC norm EN 50128. We also compare our formal approach with traditional unit testing.
Domaines
Génie logiciel [cs.SE]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...