rusu04a

V. Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. Research Report INRIA, No 5089, January 2004.

Download [help]

Download paper: Gziped Postscript

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 describes a methodology and a case study in formal verification. The case study is the protocol, a member of the adaptation layer whose main role is to perform a reliable data transfer over an unreliable communication medium. The methodology involves: (1) a state-space exploration for initial debugging; (2) a partial-order abstraction that preserves the properties of interest; and (3) a compositional verification of the properties at the abstract level using the theorem prover. Steps (2) and (3) guarantee that the properties still hold on the whole (composed, concrete) system as well. The value of the approach lies in adapting and integrating several formal techniques for verifying a real case study

Contact

Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html

BibTex Reference

@TechReport{rusu04a,
   Author = {Rusu, V.},
   Title = {Verifying an ATM Protocol Using a Combination of Formal Techniques},
   Number = {5089},
   Institution = {INRIA},
   Month = {January},
   Year = {2004}
}

EndNote Reference [help]

Get EndNote Reference (.ref)