Verifying an ATM Protocol Using a Combination of Formal Techniques - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2003

Verifying an ATM Protocol Using a Combination of Formal Techniques

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-5089.pdf (438.4 Ko) Télécharger le fichier

Dates et versions

inria-00071494 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00071494 , version 1

Citer

Vlad Rusu. Verifying an ATM Protocol Using a Combination of Formal Techniques. [Research Report] RR-5089, INRIA. 2003. ⟨inria-00071494⟩
47 Consultations
228 Téléchargements

Partager

Gmail Facebook X LinkedIn More