Integrating Formal Verification and Conformance Testing for Reactive Systems

Abstract : In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system— an extended input-output automaton, which may be infinite-state—and a set of safety properties (“nothing bad ever happens”) and possibility properties (“something good may happen”) are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a Bounded Retransmission Protocol.
Type de document :
Article dans une revue
IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2007, 33 (8), pp.558-574. 〈10.1109/TSE.2007.70707〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00422904
Contributeur : Hervé Marchand <>
Soumis le : jeudi 8 octobre 2009 - 15:11:02
Dernière modification le : mercredi 29 novembre 2017 - 16:21:09
Document(s) archivé(s) le : mardi 15 juin 2010 - 21:49:13

Fichier

2007-IEEE-TSE.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Camille Constant, Thierry Jéron, Hervé Marchand, Vlad Rusu. Integrating Formal Verification and Conformance Testing for Reactive Systems. IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2007, 33 (8), pp.558-574. 〈10.1109/TSE.2007.70707〉. 〈inria-00422904〉

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

315