Abstract:

Applying formal methods to testing has recently become a quite popular
research topic. In this paper we explore the opposite approach, namely,
applying testing techniques to formal verification. The idea is to use
test generation techniques to extract subsets (called components) from a
specification and to perform the verification on the components rather
than on the whole system. This may considerably reduce the verification
effort and, under reasonable sufficient conditions, a safety property
verified on a component also holds on the whole specification. 

We demonstrate the approach by verifying an electronic purse system using
our symbolic test generation tool STG and the PVS theorem prover.



Contents: 

ceps.dmp:     PVS 2.3 dumpfile for the query and create/update functions
              of the CEPS (common electronic purse system). Includes PVS
              specifications, theorems, and proofs, and a large library of 
              finite sets (also available on SRI International's PVS site
              at ftp://pvs.csl.sri.com/pub/pvs/libraries/finite_sets.dmp).
              PVS 2.3 is available at http://pvs.csl.sri.com.

              The library employed here is a slightly augmented version of
              the public one. To replay the proofs: save the ceps.dmp file 
              in a directory DIR. The finite sets library should go in a 
              subirectory of DIR called finite_sets. Then, launch PVS 2.3. 
              Type ESC-x undump-pvs-files then load the ceps.pvs file into
              your main emacs window, and type ESC-x prove-importchain. 
              
              This replays the proof of every statement 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.3 patch level 1.2.2.102 on Linux.
              


allslots.if: IOSTS representation of the CEPS all-slots query function
             (automatically generated by the STG tool)

ceps.if:    The IOSTS specification of the CEPS


create_update.if : IOSTS representation of the CEPS create_update function
                    (automatically generated by the STG tool)

slides.ps : slides of presentation.

PDF files : "natural language" specification of the CEPS, from www.cepsco.org.