Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Hervé Marchand Connect in order to contact the contributor
Submitted on : Thursday, October 8, 2009 - 3:11:02 PM
Last modification on : Friday, February 4, 2022 - 3:19:12 AM
Long-term archiving on: : Tuesday, June 15, 2010 - 9:49:13 PM


Publisher files allowed on an open archive



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⟩



Record views


Files downloads