%0 Conference Proceedings
%F rusu03b
%A Rusu, V.
%T Compositional verification of an ATM protocol
%B Formal Methods Europe (FME'03)
%X Abstraction and compositionality are key ingredients for the successful verification of complex infinite-state systems. In this paper we present an approach based on these ingredients and on theorem proving for verifying communication protocols. The approach is implemented in PVS. We demonstrate it by verifying the data transfer function of the SSCOP protocol, at ATM protocol whose main requirement is to perform a reliable data transfer over an unreliable communication medium
%U http://www.irisa.fr/vertecs/Publis/Ps/2003-FM.ps.gz
%D 2003