PI-1596: Verifying an ATM Protocol Using a Combination of Formal
Techniques
Vlad Rusu
http://www.irisa.fr/bibli/publi/pi/2004/1596/1596.html
39 pages - janvier 2004

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) 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 PVS 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.

Résumé
Cet article présente une méthodologie et une étude de cas en
vérification formelle. L'étude de cas est le protocole SSCOP, qui
appartient à la couche d'adaptation ATM, dont la fonction principale est
d'assurer une transmission de données fiable à travers un médium de
communication non fiable. La méthodologie implique : (1) une exploration
de l'espace d'états par simulation, pour le débogage initial du système
; (2) une abstraction basée sur des ordres partiels, qui préserve les
propriétés à vérifier ; et (3) une vérification compositionnelle des
propriétés au niveau abstrait en utilisant l'assistant de preuve
PVS. Les étapes (2) et (3) sont définies de telle manière que les
propriétés vérifiées au niveau abstrait restent valides au niveau
concret. La valeur de l'approche réside dans la combinaison de
différentes techniques, qui, mises ensemble, permettent de vérifier un
système de taille réelle.

Keywords: Partial-order abstraction, compositional deductive
verification, PVS, SSCOP protocol

Mots clefs: Ordres partiels, vérification compositionnelle et déductive,
PVS, protocole SSCOP