%0 Conference Proceedings
%F rusu05a
%A Rusu, Vlad
%A Marchand, Hervé
%A Jéron, Thierry
%T Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems
%B Formal Methods 2005 (FM05)
%E Fitzgerald, John
%E Tarlecki, Andrzej
%E Hayes, Ian
%V 	 3582
%P 189-204
%S LNCS
%I Springer
%X 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
%U http://www.irisa.fr/vertecs/Publis/Ps/final.pdf
%U http://dx.doi.org/10.1007/11526841_14
%8 July
%D 2005