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.
Type de document :
Article dans une revue
The Computer Journal, Oxford University Press (UK), 2006, 49 (6), pp.710-730
Liste complète des métadonnées

https://hal.inria.fr/inria-00527571
Contributeur : Mister Dart <>
Soumis le : mardi 19 octobre 2010 - 16:02:24
Dernière modification le : mercredi 29 novembre 2017 - 15:08:13

Identifiants

  • HAL Id : inria-00527571, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

85