rusu-computer-journal

v. Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. Computer Journal, 49(6):710-730, November 2006.

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

Contact

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

BibTex Reference

@article{rusu-computer-journal,
   Author = {Rusu, v.},
   Title = {Verifying an ATM Protocol Using a Combination of Formal Techniques},
   Journal = {Computer Journal},
   Volume = {49},
   Number = {6},
   Pages = {710--730},
   Month = {November},
   Year = {2006}
}

EndNote Reference [help]

Get EndNote Reference (.ref)