HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Verifying an ATM Protocol Using a Combination of Formal Techniques

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00071494
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 5:44:53 PM
Last modification on : Friday, February 4, 2022 - 3:14:37 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:19:28 PM

Identifiers

  • HAL Id : inria-00071494, version 1

Collections

Citation

Vlad Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. [Research Report] RR-5089, INRIA. 2003. ⟨inria-00071494⟩

Share

Metrics

Record views

43

Files downloads

191