In [gimblett2004], major parts of the ep2 system have been formalized in CSPCASL [cspcasl]. Following the structure of the original ep2 documents [ep2docs], the specifications presented in [gimblett2004] can be classified to be e.g. on the Architectural Level, on the Abstract Component Description Level, or on the Concrete Component Description Level. In this context, tool support is needed to prove (1) deadlock freedom for the interaction between the various ep2 components and (2) refinement relations between the different level of abstraction.
Translating the data part of the specifications given in [gimblett2004] into adequate Isabelle code, we obtain specifications in the input format of CSPProver. Fig.2 shows a part of [ep2_nucleus.thy] (which is the nucleus of [ep2_acl.thy]) of the initialisation procedure of the ep2 Terminal at the Abstract Component Description Level.
 (*
data part *)
 typedecl
init_d typedecl request_d
 typedecl response_d typedecl exit_d
 datatype Data = Init init_d  Exit exit_d  Request request_d  Response response_d
 datatype
Event = c Data

 (*
process part *)
 datatype
ACName = Acquirer  AcConfigManagement  Terminal 
TerminalConfigManagement
 consts
ACfun :: "ACName => (ACName, Event) proc"
 primrec

"ACfun Acquirer = c ? x:(range Init) > $AcConfigManagement"

"ACfun AcConfigManagement

= c !? exit:(range Exit) > SKIP ~

c !? request:(range Request) > c ? response:(range Response) >
$AcConfigManagement"

"ACfun Terminal = c !? init:(range Init) >
$TerminalConfigManagement"

"ACfun TerminalConfigManagement

= c ? x > IF (x:range Request)

THEN c !? response:(range Response) > $TerminalConfigManagement

ELSE IF (x:range Exit) THEN SKIP ELSE STOP"
 defs
(overloaded)

Set_ACfun_def [simp]: "PNfun == ACfun"
 consts
AC :: "(ACName, Event) proc"
 defs
AC_def: "AC == ($Acquirer [range c] $Terminal)"
 defs
FPmode_def [simp]: "FPmode == CMSmode"
Fig.2.
ep2 Specification at the Abstract Component Description Level.
The Terminal starts
the initialization (line 15) and waits then for data sent by the
Acquirer. If this data is of type Request, the Terminal answers with a
value of type Response (line 18). Another possibility is that the
Acquirer wants to exit (SKIP) the initialization (line 19). Any
other type of communication sent by the Acquirer will lead to a
deadlock represented by the process STOP (line 19). On the other end of
the communication, after receiving an initialization request (line 11)
the Acquirer internally decides if it wants to exit the process (line
13) or interact with the Terminal by sending a request followed by a
response of the Terminal (line 14). The system AC to be analyzed here
consists of the parallel composition of the Terminal and the Acquirer
synchronized on the channel c (line 25).It is the defining characterization of the Abstract Component Description Level that the data involved is loosely specified. No specific values are defined (lines 25). Semantically this means that  depending on the interpretation of e.g. the type init_d  the described systems might involve infinite nondeterminism, e.g. if the type init_d has infinitely many values, the Terminal process of Fig.2. chooses internally between sending any of these values (line 15). Thus, CSPProver has simulateneously to deal with a class of specifications: it has to prove that a certain property holds for any possible interpretation of the types involved.
Using CSPProver, we can show the above described process AC to be stablefailure refinement of the process Seq given in Fig.3. Note that Seq is a sequential, i.e. by syntactic characterization deadlockfree process. As stable failure refinement preserves deadlocks, establishing this refinement proves that the interaction of Terminal and Acquirer on the Abstract Component Description Level is deadlock free. Fig.4 shows the complete script to prove the stablefailure refinement Seq =F AC (line 14) in CSPProver. First, a mapping is defined from the process names in Seq to process expressions in AC (line 35). It is hard to automatically derive such corrensondences. However, CSPProver offers assistence for easy cases. Next, it is shown that the involved recursive processes are guarded and do not use the hiding operator. This is a fully automated routine work (lines 811). After these preparations, Seq =F AC is given as a goal (line 14). Using the above mapping, now the recursive processes are unfolded to a base case and step cases by fixed point induction (line 16). Since a step case is produced for each of the process names of Seq, the step cases are instantiated by induction on SeqName (line 18). Finally, the theorem is proven by Isabelle's method auto, CSPProver's method cspF_auto, which transforms any expression into a head sequential form, and cspF_decompo, which decomposes CSPoperators, etc (line 20). See the UserGuide for more details of CSPlaws and methods.
 datatype SeqName = SeqInit  Loop
 consts
Seqfun :: "SeqName => (SeqName, Event) proc"
 primrec

"Seqfun SeqInit = c !? init:(range Init) > $Loop"

"Seqfun Loop = c !? exit:(range Exit) >
SKIP ~

c !?
request:(range Request) > c !? response:(range Response) >
$Loop"
 defs
(overloaded)

Set_Seqfun_def [simp]: "PNfun == Seqfun"
 consts
Seq :: "(SeqName, Event) proc"
 defs Seq_def: "Seq == $SeqInit"
Fig.3. A sequential process equal
to the
process shown in Fig.2.
[gimblett2004] A. Gimblett, M. Roggenbach,
and H. Schingloff. Towards a formal specification of an electronic
payment system in CSPCASL. WADT 2004, LNCS, (to be appeared) (* expected correspondence of process
names in Abs to AC *)
 consts
Seq_to_AC :: "SeqName => (ACName, Event) proc"
 primrec

"Seq_to_AC (SeqInit) = ($Acquirer [range c] $Terminal)"

"Seq_to_AC (Loop) = ($AcConfigManagement [range c]
$TerminalConfigManagement)"
 (* guarded and no hiding operator *)
 lemma
guardedfun_AC_Seq[simp]:

"guardedfun ACfun"

"guardedfun Seqfun"
 by
(simp add: guardedfun_def, rule allI, induct_tac p, simp_all)+
 (* the main thorem *)
 theorem
ep2: "Seq =F AC"
 apply
(unfold Seq_def AC_def)
 apply
(rule cspF_fp_induct_left[of _ "Seq_to_AC"])
 apply
(simp)+
 apply
(induct_tac p)
 apply (cspF_auto  rule cspF_decompo_ref  auto simp add: image_iff)+
 done
Fig.4. The complete proof script
for Seq =F AC.
In the more complex version [ep2_acl.thy], Abs <=F AC can be similarly proved by CSPProver. Furthermore, it can be proven in [ep2_ccl.thy] that Concrete Component Description Level (CC) refines Abstract Componet Level (AC), thus for all p, AC <=F CC p, where p is the initial value. Hence, we also know for the Concrete Component Description Level that the dialog between Terminal and Acquirer of the formal ep2 specification presented in [gimblett2004] does not give rise to a deadlock of the ep2 system. The theory files used here are summarized as follows:
ep2_nucleus.thy The nucleus of ep2 verification
ep2_nucleusDF.thy The verification of deadlockfreeness of ep2 by DFP
ep2_acl.thy Abstract Componet Level (AC) refines an abstraction (Abs).
ep2_ccl.thy Concrete Component Description Level (CC) refines Abstract Componet Level (AC),
References
In the more complex version [ep2_acl.thy], Abs <=F AC can be similarly proved by CSPProver. Furthermore, it can be proven in [ep2_ccl.thy] that Concrete Component Description Level (CC) refines Abstract Componet Level (AC), thus for all p, AC <=F CC p, where p is the initial value. Hence, we also know for the Concrete Component Description Level that the dialog between Terminal and Acquirer of the formal ep2 specification presented in [gimblett2004] does not give rise to a deadlock of the ep2 system. The theory files used here are summarized as follows:
ep2_nucleus.thy The nucleus of ep2 verification
ep2_nucleusDF.thy The verification of deadlockfreeness of ep2 by DFP
ep2_acl.thy Abstract Componet Level (AC) refines an abstraction (Abs).
ep2_ccl.thy Concrete Component Description Level (CC) refines Abstract Componet Level (AC),
References
[cspcasl] M. Roggenbach. CSPCASL  A new integration of process algebra and algebraic specification. AMiLP 2003. pp.229243. 2003.
[ep2docs] eft/pos 2000 Specification, version 1.0.1, EP2 Consortium, 2002.
[proofgeneral] David Aspinall. Proof General: A Generic Tool for Proof Development. TACAS 2000, LNCS 1785, pp.3842, 2000.