Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

rusu04d

V. Rusu, H. Marchand, T. Jéron. Verification and Symbolic Test Generation for Safety Properties. Research Report IRISA, No 1640, August 2004.

Download [help]

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

This paper presents a combination of verification and conformance testing techniques for the formal validation of reactive systems. A formal specification of a system - an input-output automaton with variables that may range over infinite domains - is assumed. Additionally, a set of safety properties for the specification are given under the form of observers described in the same formalism. Then, each property is verified on the specification using automatic techniques (e.g., abstract interpretation) that are sound but not necessarily complete for the class of safety properties considered here. 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. If the verification step was successful, that is, it has established that the specification satisfies the property, then the test execution may detect the violation of the property by the implementation and the violation of the standard ioco conformance relation between implementation and specification. On the other hand, if the verification step did not conclude (i.e., it did not allow to prove or to disprove the property), then the test execution may additionally detect a violation of the property by the specification

Contact

Hervé Marchand http://people.rennes.inria.fr/Herve.Marchand/
Thierry Jéron http://www.irisa.fr/prive/jeron

BibTex Reference

@TechReport{rusu04d,
   Author = {Rusu, V. and Marchand, H. and Jéron, T.},
   Title = {Verification and Symbolic Test Generation for Safety Properties},
   Number = {1640},
   Institution = {IRISA},
   Month = {August},
   Year = {2004}
}

EndNote Reference [help]

Get EndNote Reference (.ref)