Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems

Abstract : This paper presents a combination of verification and conformance testing techniques for the formal validation of reactive systems. A formal specification of a system, which may be infinite-state, and a set of safety properties are assumed. Each property is verified on the specification using automatic techniques based on abstract interpretation, which are sound, but, as a price to pay for automation, are not necessarily complete. Next, for each property, a test case is automatically generated from the specification and the property, and is executed on a black-box implementation of the system to detect violations of the property by the implementation and non-conformances between implementation and specification. If the verification step did not conclude, the test execution may also detect violations of the property by the specification
Type de document :
Communication dans un congrès
John Fitzgerald, Andrzej Tarlecki, Ian Hayes. Formal Methods 2005 (FM05), Jul 2005, Newcastle, United Kingdom. Springer-Verlag, 3582, pp.189-204, 2005, Lecture Notes in Computer Science. 〈10.1007/11526841_14〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00483945
Contributeur : Hervé Marchand <>
Soumis le : lundi 17 mai 2010 - 15:14:21
Dernière modification le : vendredi 27 octobre 2017 - 01:08:52
Document(s) archivé(s) le : jeudi 16 septembre 2010 - 14:37:41

Fichier

fm05.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Vlad Rusu, Hervé Marchand, Thierry Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. John Fitzgerald, Andrzej Tarlecki, Ian Hayes. Formal Methods 2005 (FM05), Jul 2005, Newcastle, United Kingdom. Springer-Verlag, 3582, pp.189-204, 2005, Lecture Notes in Computer Science. 〈10.1007/11526841_14〉. 〈inria-00483945〉

Partager

Métriques

Consultations de la notice

181

Téléchargements de fichiers

87