Skip to Main content Skip to Navigation
Journal articles

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 SSCOP protocol, a member of the ATM adaptation layer whose main role is to perform a reliable data transfer over an unreliable communication medium. The methodology involves: (1) simulation for initial debugging; (2) partial-order abstraction that preserves the properties of interest; and (3) compositional verification of the properties at the abstract level using the PVS theorem prover. Steps (2) and (3) guarantee that the properties still hold on the whole (composed, concrete) system. The value of the approach lies in adapting and integrating several existing formal techniques into a new verification methodology that is able to deal with real case studies.
Document type :
Journal articles
Complete list of metadata
Contributor : Mister Dart Connect in order to contact the contributor
Submitted on : Tuesday, October 19, 2010 - 4:02:24 PM
Last modification on : Friday, February 4, 2022 - 3:22:46 AM


  • HAL Id : inria-00527571, version 1



Rusu Vlad. Verifying an ATM Protocol Using a Combination of Formal Techniques. The Computer Journal, Oxford University Press (UK), 2006, 49 (6), pp.710-730. ⟨inria-00527571⟩



Record views