Verifying an ATM Protocol Using a Combination of Formal Techniques

  (improved version of a paper presented at Formal Methods Europe'03)

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.

-report.ps:  extended version of a paper presented at FM'03 (work in progress)

-paper-FM.ps:  earlier  version (in  Formal  Methods Europe'03, LNCS 2805)

-talk.ps: slides from talk at FM'03

-sscop.DMP:   PVS 2.4 dump file for the case study. Includes PVS specifications,
              theorems, and proofs for the case study.

              To replay the proofs: save the sscop.DMP file in a directory. Then, 
              launch PVS 2.4. Type ESC-x undump-pvs-files then load the sscop.pvs 
              file into your main emacs window, and type ESC-x prove-importchain.
              
              This replays the proof of every theorem for the case study. For some 
              reason (different numbering of formulas) this may  not work very well 
              with other versions of PVS. The version used here is PVS Version 2.4
              patchlevel 1, available free of charge at http://pvs.csl.sri.com.

              There are ~230 theorems to prove (and, additionally ~400 trivial type 
              correctness conditions, automatically generated and proved  by PVS). 
              Replaying the proofs takes a few hours.