Verifying an ATM Protocol Using a Combination of Formal Techniques *A preliminary version of this paper has appeared in Formal Methods Europe (FME'03), LNCS 2805, pp 223–243. The URL http://www.irisa.fr/vertecs/Equipe/Rusu/sscop contains PVS ...

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 (i) simulation for initial debugging; (ii) partial-order abstraction that preserves the properties of interest and (iii) compositional verification of the properties at the abstract level using the PVS theorem prover. Steps (ii) and (iii) 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. [ABSTRACT FROM PUBLISHER]