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


Vlad Rusu, Hervé Marchand, Thierry Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. In Formal Methods 2005 (FM05), John Fitzgerald, Andrzej Tarlecki, Ian Hayes (eds.), LNCS, Volume 3582, Pages 189-204, July 2005.

Download [help]

Download paper: Doi page

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


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


Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html
Hervé Marchand http://www.irisa.fr/prive/hmarchan
Thierry Jéron http://www.irisa.fr/prive/jeron

BibTex Reference

   Author = {Rusu, Vlad and Marchand, Hervé and Jéron, Thierry},
   Title = {Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems},
   BookTitle = {Formal Methods 2005 (FM05)},
   editor = {Fitzgerald, John and Tarlecki, Andrzej and Hayes, Ian},
   Volume = {    3582},
   Pages = {189--204},
   Series = {LNCS},
   Publisher = {Springer},
   Month = {July},
   Year = {2005}

EndNote Reference [help]

Get EndNote Reference (.ref)

| VerTeCs | Team | Publications | New Results | Softwares |
Irisa - Inria - Copyright 2005 © Projet VerTeCs