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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Rusu, V., Marchand, H., & Jéron, T. (2005). Automatic verification and conformance testing for validating safety properties of reactive systems. In Lecture Notes in Computer Science (Vol. 3582, pp. 189–204). Springer Verlag. https://doi.org/10.1007/11526841_14
Mendeley helps you to discover research relevant for your work.