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

Vlad Rusu (1) , Hervé Marchand (1) , Thierry Jéron (1)

1 VERTECS - Verification models and techniques applied to testing and control of reactive systems

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

Domaines: Génie logiciel [cs.SE]

Vlad Rusu, Hervé Marchand, Thierry Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. Formal Methods 2005 (FM05), Jul 2005, Newcastle, United Kingdom. pp.189-204, ⟨10.1007/11526841_14⟩. ⟨inria-00483945⟩