Home

Compositional Verification of a Network of CSP Processes: using

1. The above result allows us to proceed to automatic verification of condition RE 9 4 Verification in practice It is possible to construct the process FINALIMPLE in such a way in practice that we avoid the state explosion which may arise from first composing in parallel the disjoint processes RE to give RE and then composing RE in parallel with Q we use this order of composition above for simplicity of reasoning By associativity of the parallel composition operator we have that Q RE Q RE RE2 REz where processes channel sets and renamings are subscripted it is assumed that the subscript is taken from the set I and J is used to denote the cardinality of I Due to the way extract is defined in terms of extract and since extract refers only to events in RE we may push the extract components inwards as far as possible over the parallel composition We may do the same with the hiding of aBnia and the renaming using m for the same reason and thus have the following result Q REz extract aBnia m Q RE1 extract aB m RE2 eztract aB2 m RE 7 extract7 Biz m This new order of composition of the necessary component processes means that we keep down the size of the intermediate processes constructed by FDR2 as FINALIMPLE itself is constructed Compositional Verification using FDR2 31 9 5 Example We now sh
2. We now define renaming functions domain and extract as follows domain U domaini and extract U extracti icI icI Note that domain and extract are well defined by the disjointness of aB and aB when i j It is unnecessary to define processes TE for the identity extraction patterns ep where b big since for traces over events in aB ab the extraction mapping eztr is simply the identity mapping We thus define TE as TE lier TE Although it may not be immediately obvious the alphabets of distinct TE are disjoint This dis jointness which is due to the disjointness of the aB and also the disjointness of the ab can be easily observed from the following lemma Lemma 13 aTE A U Ag where Ay a a aB A It to a Dom A extr t extr to a and A Ag extract chan data bj val da chan data E aB e b val abj t E Dom to a Dom eatr t o e eatr to a Proof The proof is immediate from the definitions above of m and Corollary 14 fi 4 j then aTE NaTE 0 Compositional Verification using FDR2 17 Extracting the traces of Q Once TE has been defined we wish to compose it in parallel with Q before applying the hiding and renaming which will mimic the application of the extraction mapping In order for Q to synchronize with TE we have to rename its events each event of Q is renamed to all those events in a TE
3. P R is a proper subset of aP All inputs to FDR2 must be supplied in the machine readable syntax of CSP See 15 or the FDR2 manual 7 for details Although we will define processes syntactically in this paper using the standard CSP syntax all of the operators used have a direct equivalent in the machine readable syntax Note however that the operator in the machine readable syntax which represents parallel composition must be provided explicitly with the events on which synchronization is to occur to mimic the parallel composition operator used here it is simply necessary to provide the set of events in the intersection of the alphabets of the two processes to be composed 3 Extraction patterns and the implementation relation 3 1 Extraction patterns In this section we first explain the basic mechanism behind our modelling of behaviour abstraction extraction patterns and then provide a formal definition of these objects The example given here which is used as a running example in the remainder of the paper is deliberately very simple in order to better convey the basic ideas rather than to demonstrate a wider applicability of the approach in gt Sendspec mid Bufspec out in Sendimpie oe Bufimpte out ac a b Fig 1 A simple specification network and its implementation Consider a pair of specification or base processes Send spec and Buf sp
4. d dr ab C X Note by definition of dz that if d D X then b Dnia Lemma 27 The following hold of NEWSPEC 1 aNEWSPEC aP U dr 2 NEWSPEC t R Alt X 6 P RC X N abia U D X U abnia 3 TNEWSPEC TP Ufto di tETP A di dy Proof 1 We have that aP aPU prime abnia and PROC abnia U prime abnia U dr From this we have that aP aP U prime abniq U dr and the proof of this part follows from the definition of m 2 We first have that oP t R G w X oP p t w A RC X Uprime X Nabnia We then observe that Oacabaa gt PROC O DIV a o s R a E abnia A s R E PROC Oacprime abnia gt DIV R R C abnia U dr In order to determine the events which are refused here we assume that a Ogeprime abniag t gt DIV aPROC Gyeary gt DIV O DIV b Compositional Verification using FDR2 27 It follows that PROC t R t E abnia A R C abnig U dr From the above we have that oP t R G X 4P R C X N abia U prime X N abnia U abnia U dr The proof of this part follows by the definition of m the semantic definition of the renaming operator see section A in the appendix and recall that m d prime aB U prime ab and the fact that 6 P P since P 3 We first have that tP t p t rP We then observe
5. H R Simpson Four slot Fully Asynchronous Communication Mechanism IEE Proceedings 137 Pt E 1 January 1990 17 30 Operator definitions first show how the alphabet of a process may be derived from the alphabets of its components ala P a UaP a P OQ aPUadq a P N Q aPUaQ a P Q aPUaQ a P A aP A a P R R aP The traces model In order for a set of execution sequences to be considered a valid process in the traces model they must meet a consistency condition T1 TP is non empty and prefix closed The semantics of a process term in the traces model may be derived recursively from the semantics of its components and the semantic definition accorded to the various operators used to combine those components 34 J Burton T a gt P U a os serP T POQ TPUTQ T P N Q TPUTQ T P Q t tlaPETP A thaQe7Q T P A t A terP T P R t du e7P uR t The stable failures model The set of failures and traces representing a process in the stable failures model have to meet the following consistency conditions SF1 TP is non empty and prefix closed SF2 t R P gt teErP SF3 t R E OP ASCR t S OP SF4 t R E dP A to a g TP t RU a OP The necessary semantic definitions of the various operators in the stable failures model are as follows note that the effect of the various operators on the trace component of the model is as
6. Qzeqo 1 data z gt RE x O DIV N RE X Y lye adataprimeUaackprime R y gt DIV RE x eztractack yes mid x RE DO ack no gt RE x O DIV RE x extractdata mid x gt RE O DIV Using the components defined above and the renamings extract and prep as described in section 6 2 we were able to define the necessary process expressions By supplying them as inputs to FDR2 we were then able to verify automatically that Bufimpie respectively Sendimpie meets condition RE with respect to Bufspec respectively Sendspec 10 Concluding remarks We have developed a verification method that allows for automatic compositional verification of networks of CSP processes in the event that corresponding specification and implementation processes have different interfaces Most importantly we have built that method of verification on top of an existing industrial strength tool with all the benefits which that accrues Although the approach may seem somewhat unwieldy if a user is required to provide explicitly the various components used to produce the inputs to FDR2 it is relatively straightforward to automate production of these inputs from the input which the user must necessarily supply In other words the user supplies the original specification and implementation components the necessary extraction pattern representations not incorporating refusal boun
7. TQ The proof of this part follows from the above Before going on to define the tester process which will be composed with Q to give a process which will deadlock if and only if Q does not meet condition LC with respect to channel b we first give some preliminary definitions and results 8 1 Preliminary definitions and results The following results and definitions will be used in giving the semantic characterisation of the process to be composed with Q and to show that it does indeed encode exactly the properties we wish These definitions will also be used when we come to consider condition RE In what follows the set of maximal Compositional Verification using FDR2 21 refusal bounds for a particular extraction pattern ep and trace t Dom is denoted as RM R Re refit A VR refit RER gt R RP The mapping Off Dom 2 is used to define the possible sets of events one of which must be offered in its entirety by a receiver process on the channel set B after a trace t t B Z dom if it is to meet condition LC with respect to channel b That is it gives all possible sets of events which include a single event from each set of events one of which must be offered by a sender process over B when its refusals are constrained by ref We define OF Y Y CaB A VRE RM Aa Y ag R and impose the restriction that all sets in Off t are minimal under the subset ordering
8. aca We then compose Q in parallel with PROC with the result that for every failure t R Q the refusal R has aQ aB added to it This means that the refusal R N aB will survive the hiding of the events in aQ aB This gives us the following process Qi Q PROG a aB Note in part 2 of the following lemma that w X 1Q rather than simply Q This means that we can look at the meaning of the process expression Q in the stable failures model rather than in the failures divergences model and yet we will not lose any failures information by doing so recall that the conditions of the implementation relation itself are defined in terms of the failures divergences model This is the fact that allows us to work only in the stable failures model and thus to transform the checking of condition LC into a check for deadlock freedom Lemma 20 The following hold of Qi 1 aQ aB x 2 Qi t R G w X 1Q t w Bi A RC aB NX 3 TQ t weT At wl B Proof 1 We observe that aPROC aQ and the proof of this part follows immediately 2 By theorem 7 and the fact that conditions DP and DF have been met sQ and so 4Q 61 We observe that PROC t R R C aQ aB From this we have that 4 Q PROC t R A t X 41 RC aQ aB U aB N X The proof of this part follows from the above 3 We first observe that tPROC aQ and from this we have that r Q PROC
9. chronous communication between processes in such a way that each of them is free to engage indepen dently in any action that is not in the other s alphabet but they have to engage simultaneously in all actions that are in the intersection of their alphabet The operators O M and are all commutative and associative and may be indexed over finite sets 4 J Burton Let P be a process and A be a set of events then P A is a process that behaves like P with the actions from A made invisible Note that the operator is overloaded since it is also used to denote set subtraction Hiding is associative in that P A A P AU A If t is a trace of a process P then t A t aP A Let R be a relation and P a process Then P R is a process that behaves like P except that every action a has been replaced by R a note that the relation R does not need to be total over the alphabet of P and if a is not in the domain of R we assume that R a a R a will return a set of values and so wherever the action a might have been enabled in P each of the events in R a will be enabled in its place in P R The definition of R extends to traces and sets in the obvious way We define R as follows a1 an R bi bm n MAM lt n a Rb And R A U R a The semantic definitions of the above operators may be found in section A in the appendix acA We now give details of the process models we will use In what fo
10. s 6P R 6 P R s ot ds P sR s
11. Uacap rX E aB a X S S RefSets t Proof C Let X Mrermi Usean rtX a X It follows that for every R RM there exists a aB R such that a X As a result there exists Y Off t such that Y N X Q It follows that X C aB Y and so X RefSets t 2 Let S RefSets t We have that S C aB Y for some Y Off t We therefore have that SOY and so for every R RM there exists a R such that a Y and so a S It follows that for every R RM there exists a aB R such that a S The proof in this direction follows from the above 8 2 The tester process for channel set B We now define the tester process LCEP which has exactly the traces of Dom and exactly the refusals allowed by RefSets After a trace t dom in LCEP we may arrive non deterministically at one of two types of state At the first are enabled all events which are valid extensions of t with respect to Dom This ensures that 7D CEP contains all of the traces of Dom That this type of state does not contribute to a failure of LCEP is ensured by the appearance of DIV as an argument to the deterministic choice operator The other type of state is used to generate the refusals which are allowed by RefSets t after an event has been executed from one of these second type of state we proceed to a state which is equivalent to the immediately diverging process This means that the second
12. epuep TQ CrP For ease of expression and manipulation the above results imply that we would compose the extrac tion pattern representations TE such that i I in parallel and then compose the result with Q This would be inefficient since the composition of the extraction pattern processes all of which are disjoint could be very large indeed As a result we would compose each such process with Q individually We are able to do this since parallel composition is associative 18 J Burton 6 2 Example Here we show how to apply the results in this section to verify that Bufimpie meets condition TE with respect to Buf Note that the components defined here could be used equally well without modification to verify that Sendimpie meets condition TE with respect to Sendspec since condition TE is not concerned with whether channel b for extraction pattern ep is an input or an output channel This contrasts with condition LC for example which does distinguish between input and output channels Let Q be Bufimpie after the application of the necessary preprocessing Let ep be ePtwice Note that B data ack We define the process TE as follows TE xe 0 1 data x exrtractacr yes mid 2 TE O ack no extractgata c mid c gt TE We then give the concrete renamings prep and extract used in this example ack yes extractack yes mid 0 ack yes extractack y
13. important because corollary 4 5 only refers to stable failures of Q LC We consider each b brig in turn and show that if condition LC is not violated in Q by b then neither is that condition violated by b in Q Let t R E DomQ t X E DomQ be as characterised in corollary 4 5 and let b bnia We consider each of two cases in turn Case 1 b is not blocked at t X in Q It follows from the contrapositive of lemma 5 that b is not blocked at t R in Q Case 2 b is blocked at X in Q In this case it follows that t B E dom and the proof is immediate P x RE Let t R E daomQ We know that t R Q Let t X Q be as characterised in corollary 4 5 We also have that t X domQ By definition of condition RE it suffices to show that any channel bi bnia is blocked at t X in Q if it is blocked at t R in Q and also that RNabia XNab ia That the former requirement is met follows from lemma 5 The latter requirement is met due to corollary 4 5 d Let Q lt e P We establish that Q lt P by considering each of the conditions in turn DP GE TE The proof follows from corollary 4 1 and 4 3 DF The proof follows from corollary 4 2 and 4 3 It follows that DomQ C Q and also daomQ C QQ This is important because corollary 4 4 only refers to stable failures of Q LC RE We prove a contradiction Assume that t R E dpomQ t R E daom is a failure at which condition LC RE i
14. X RE t o domain a Case 1b t dom In this case we have that RE t a o s X a mit A s X ORE to domain a U Urermjt R R C prep aB U prime R Case 2 b out P Case 2a t Dom dom In this case we have that RES t a 0 s X a a t A s X OREO t o domain a Case 2b t dom In this case we have that RES t a o s X a mi t A s X PRES t o domain a U Orermi Useprime aB R iO X a g XAXE prep aB U prime aB From a straightforward induction on the length of traces using the above two cases and the definitions of extract and 7 and lemmas 22 and 23 we have that RE t R domain t dom A extract t aB extr domain t A AR RefSets domain t R C prep aB U prime R The proof of this part follows from the above and EP5 EP6 and EP7 3 We begin by considering each of two cases in turn Case 1 b in P Case la t Dom dom In this case we have that TRE t U a os ae m t A s ETRE to domain a Case 1b t dom In this case we have that TRE t U a os a r t A s TRE to domain a U prime a AR RM a R Case 2 b out P Case 2a t Dom dom In this case we have that TREO t U la os aem t A s TREO to domain a Case 2b t dom In this case we have that TREO t U la os
15. a r t A s TREO to domain a U prime a IR RMj a Z R From a straightforward induction on the length of traces using the above two cases and the definitions of extract and 7 along with the third clause given in cases 1b and 2b respectively and EP4 we have that TRE t domain t Dom A extract t aB extr domain t U to prime a domain t dom A extract t aB extr domain t A domain t o a Dom The proof of this part follows from the above and EP5 EP6 and EP7 We now define the process FINALIMPLE which will constitute the implementation process supplied to the refinement check in FDR2 which will check whether or not Q meets condition RE with respect Compositional Verification using FDR2 29 to P It is defined in terms of an auxiliary process PREIMPLE simply to make clearer the presentation of proofs below and also for the purposes of the readability of the definition itself PREIMPLE Q RE extract aBnia FINALIMPLE PREIMPLE n We define block w X d dy b is blocked at w X Remember that if d dy then b bnia Lemma 29 The following hold of FINALIMPLE 1 aFINALIMPLE aP Udy n 2 FINALIMPLE t R E w X daom eztr epuep w t A RC X Nabja U block w X U abnia 3 TFINALIMPLE extr epuep TQ U to di Gw o a TQ bi bnid EXtT epuep w t Aa aB A wl B d
16. an event from ab i e the events from the specification which ep can interpret as having occurred after extraction If we project the traces from TE using renaming onto the left hand event of each pair then we get the traces of Dom If we project using hiding and renaming onto the right hand event of each pair then we get the traces representing extr Dom Note that the notions of left hand and right hand event are used purely for ease of expression and have no other significance Since CSP has no operator itself which allows direct definition of a function from traces to traces then the user must define the process TE explicitly rather than simply applying some operator to a process which encodes Dom where b bnia that is the user has to encode the extraction function explicitly 6 1 Extraction pattern construction We now show how to construct the process TE The main problem to address is the nature of the events that will be used necessarily within the syntax of machine readable CSP to represent the pairs of events described informally above In machine readable CSP events are of the form channelname dataval where dataval is a value of type datatype and datatype is the type of the channel channelname Note Compositional Verification using FDR2 15 that datatype may be an empty data type leaving the channel name as a simple event in this case dataval is not used a simple data type or a
17. avoid ambi guity In what follows different extraction patterns will have disjoint sources and distinct targets For notational convenience we lift some of the notions introduced to finite sets of extraction patterns Let ep epi ep be a non empty set of extraction patterns where ep Bi bi dom extr ref Moreover let B By U U By Then EP5 dome t aB Vi lt n t Bi dom EP6 Domep t aB Vi lt n t Bi Doms EP7 eztrep and for every to a E DoMep with a aB extr ep to a extr ep t ou where u is a possibly empty trace such that extr t B o a extr t Bi o u Note that u in EP7 is well defined since extr is monotonic 3 4 The implementation relation We present here the relation from 6 which is a slightly modified version of that in 5 All proofs of results in the remainder of this section can be found in 6 Suppose that we intend to implement a base process P using another process Q with a possibly different communication interface in what follows P and Q denote process expressions The correctness of the implementation Q will be expressed in terms of two sets of extraction patterns ep and ep The former with sources in Q and targets in P will be used to relate the communication on the input channels of P and Q while the latter with sources out Q and targets out P will serve a similar purpose for the output channels Let P be a base
18. d RN abia X N abia SEEN We now give a supporting result before giving the main result of this section that Q meets all of the conditions of the implementation relation if and only if Q does Lemma 5 Let t R and t X be as characterised in corollary 4 5 If bi E bnia is blocked at t R then it is blocked at t X Proof Let b be blocked at t R We consider each of two cases in turn Case 1 b out Q By corollary 4 5 b we know that RN out Q X N out Q Since we know that aBi N R g ref t Bi it follows that aB N X ref t Bi and so b is blocked at t X Case 2 b in Q In this case if a RNAB XNaB then t Bjo a Dom by corollary 4 5 c and the definition of NotNextr By EP4 we know that if Z ref t Bi then ZU a ref t Bi Since b is blocked at t R we know that aB R ref t Bj It follows from the above that aB X ref t Bi and so b is blocked at t X Theorem 6 Let P be a specification process Then Q Zi P if and only if Q a P Proof We first note that if t R o Q and t X 1Q t R dpom if and only if t X DomQ Likewise t R dgomQ if and only if t X daomQ Let Q P We establish that Q x P by considering each of the conditions in turn DP GE TE The proof follows from corollary 4 1 DF The proof follows from corollary 4 2 It follows that pen C oQ and also baom C p This is
19. described for the traces model above ola P X a g X U a os X s X OP oP Q oPU Q POQ X 1 X PN GQ U s X 8 X PU GQ A 5 o P Q u Y UZ As t s Y oP A t 2 9Q A s ulaP A t ulaQ o P X t X Y t Y UX oP PIR s X Gs sR s A s R7 X oP The failures divergences model The set of failures and divergences representing a process in this model have to meet the following consistency conditions FD1 7 P is non empty and prefix closed FD2 R E ds PASCRSE S ECOLP FD3 t R E P A tola 7T P t RU a oP FD4 se P Ate aP gt sote oP FD5 tedP gt t R o P The definitions of the operators in the failures divergences model are as follows gi a gt P X a X U a os X s X LP la gt P a os sedP PLP 1 Q 1 PUGLQ AP NQ 6PU6Q o1 POQ XIX G1 PNG QJU 5 X 8 X G1 PUGLQ A sA U X P UQ POQ 6PU6Q osi P Q u YUZ Gs t s Y OL P A t Z EQ A s ulaP A t ul aQ U u Y u P Q API Q f uov Gser PteT Q ulaP s A ufaQ t A sEdP V tE dQ P X s X ss UX bi P U s X s 6 P X O P X s X ot sedP U u X ot ue aP A u X is finite A Vs lt u s 7 Ph bi P R s X As sR s A s R71 X OL PHU s X
20. for this extraction pattern in terms of two auxiliary processes LCEP x and LCEP x LCEP Qse4o 1 data 2 gt LCEP DIV LCEP x ack yes LCEP O ack no gt LCEP x 0 DIV N RE odata Nye aB R y gt DIV LCEP x data x gt LCEP O DIV N Orefan data c Mye aB R Y gt DIV From these process expressions we were able to define FINALIMPLE for ep eP iwice When b is an output channel and check it for deadlock freedom using FDR2 as a result of which we have checked condition LC for Sendimple 9 Checking condition RE Finally we consider how to check condition RE We assume that by this stage all other conditions of the implementation relation have been successfully verified for Q The condition to be met is as follows RE If t R E ddom then extr epuep t aB U RN abia 1 P where B C bnia is the set of all channels of P blocked at t R Compositional Verification using FDR2 25 From theorem 7 and the fact that conditions DP and DF have been met we can deduce that 5Q and so dQ Q Since we require 6P 0 then we also have that P P These two facts allow us to check condition RE while working only in the stable failures model they guarantee that we do not lose any information on the failures of either P or Q by working in that model as opposed to working in the failures divergences model remember t
21. have TLCEP t U a os a Nezti t A s TLCEP to a Case 2b t Dom dom In this case TLCEP t U a os a Nezt t A s TLCEP to a U a AR RM a R The proof of this part follows from the above by a straightforward induction on the length of traces using the definition of Nezt the definition of RM and EP4 Note in the above result that we have no stable failure with a trace component t such that t dom This is because condition LC is not interested in what is refused when behaviour over a channel set B is complete We are now in a position to define the process FINALIMPLE upon which the check for deadlock freedom will be carried out FINALIMPLE Q LCEP Theorem 25 Q meets condition LC with respect to channel b if and only if FINALIMPLE is deadlock free Proof By lemma 24 2 and lemma 20 2 we have that 6FINALIMPLE t R A w X 10 Y RefSets t t w Bi tg dom A RC aBiNX UY The proof follows immediately from the above and lemma 21 Corollary 26 Q meets condition LC if and only if for every ep such that bi bnia FINALIMPLE is deadlock free The above result allows us to proceed to automatic verification of condition LC 24 J Burton 8 3 Example We now show how to define the relevant process expressions used to verify that Bufimpie and Sendimpie respectively meet con
22. know that Q meets condition TE we know that ext epuep TQ C TP and so it follows from lemma 27 3 and lemma 29 3 that TFINALIMPLE C TNEWSPEC We simply have to show therefore that 6FINALIMPLE C NEWSPEC Let t R FINALIMPLE By lemma 29 2 there exists w X ddom such that t ext epuep wW RN abia C X Nab and if d R then b bnia is blocked at w X Since Q meets condition RE we know that there exists t Y P such that YN abia X N abia that is RN abia C Y N abia and if b bnia is blocked at w X then ab C Y By lemma 27 2 there exists t Z 6NEWSPEC such that RN abia C YN abia ZN abia di Z if abi C Y that is if b is blocked at w X then d Z and abnia C Z It follows from the above and SF3 see section A in the appendix that t R NEWSPEC lt We assume that NEWSPEC Ep FINALIMPLE and prove that Q meets condition RE under this assumption Let w X daom By lemma 29 2 there exists t R FINALIMPLE such that t ettr epuep w RN abia X N abia and d R if b bria is blocked at w X Since we assume that pFINALIMPLE C NEWSPEC we have that t R 6NEWSPEC It follows from lemma 27 2 that there exists t Y 1 P such that X N abia RN abia C Y N abia and if d E R that is if bi bnia is blocked at w X then ab C Y The proof in this direction follows from the above and SF3 see section A in the appendix
23. of which it might form the left hand component If an event may only form the left hand component of an event pair where the right hand component is the empty trace then we do not need to rename that event at all Re We now define the renaming prep aB x aTE which is applied to Q see section 6 2 for the renaming prep used when verifying condition TE for the processes which appear in the running example If a aB prep a extract chan data b val a chan data extract chan data b val a TE U a N a TE The final clause of the above definition is simply to ensure that any event a is also renamed to itself where necessary We now give the definition of the process INTERP which in the traces model has exactly the traces of Q after extraction INTERP Q prep TEr eztract aBnia Lemma 15 Q prep TEr domain r Q A A Proof C Let t 7 Q prep TEr domain Then there exists w 7 Q prep TEr such that domain w t Since aTEr C aQ prep we have that w TQ prep It follows by definition of prep that domain w t 7Q 2 Let t TQ We know that t Domepuep by lemma 10 By lemma 12 2 and EP6 there exists w E TTE such that domain w t Brig By definition of prep it follows that there exists A u T Q prep TEr such that domain u t Lemma 16 Let w t Q prep TEr and domain w t Then ertract w aBnia ext epuep t P
24. some way of relating behaviour over channels data and ack to that over mid Firstly we must relate traces and do this using a mapping extr which in this case for example would need to relate traces over data and ack to those over mid For example ae dr data v ack yes gt mid v data v ack no gt data v ack no data v Note that the mapping ertr has a well defined domain here it is only defined for traces where message transmission was successful in the first place or where retransmission must succeed We call this domain Dom Observe also that some of the traces in Dom may be regarded as incomplete For example data v is such a trace since we know that the event data v must be followed by an event on channel ack The set of all other traces in Dom i e those which in principle may be complete will be denoted by dom For our example dom will contain all traces in Dom where we know that the last value communicated on channel data has been transmitted or retransmitted successfully We also need a device to relate the refusals and so failures of Bufimpie to those of Buf This comes in the form of another mapping ref constraining the possible refusals a process can exhibit after a given trace t Dom on channels which will be hidden when the final implementation network is composed More precisely a sender process can admit a refusal disallowed by ref t only if the extracted trace extr t admits i
25. state and so finitely non deterministic gt We prove a contradiction Let t mind INTERP Since SQ by theorem 7 STE 0 by lemma 18 and neither renaming nor parallel composition can introduce divergence it follows that A PaA 6 Q prep TEr extract 0 It follows that there exists w T Q prep TEr such that w uov and Compositional Verification using FDR2 19 extract v v Bnia note that domain w TQ by lemma 15 As a result domain w aQ while extract w aBnia is finite and so extr epuep domain w is finite by lemma 16 This means that condition GE is not met by Q and so we have a contradiction N lt Since 6INTERP 6 we know that there does not exist a trace w T Q prep TEr such that w uov and eztract v v aBnia It follows from the above and lemmas 15 and 16 that for every t aQ N TQ ext epuep t is of infinite length 8 Checking condition LC The condition to be checked is as follows LC If b bnia and b is a channel of P blocked at t R E dpomQ then t B E dom We again assume that conditions DP and DF have been verified successfully by this point From this and theorem 7 we can deduce that 6Q and so 4Q Q Below we transform the check for condition LC into a check for deadlock freedom on a process derived from Q Since deadlock freedom is checked in the stable failures model we are only able to effect t
26. that T Oacab aa gt PROC O DIV U a os a abnia A s E TPROC T a prime abnia gt DIV U a a prime abnia T Oyeay gt DIV O DIV U a a dr It follows that TPROC abnia U to a t abnia A a prime abnia U to di te abnia A di dr From the above we have that TP TPU to a to b ETP A bE abria A a prime b U to di Ite TP A AGE dr The proof of this part follows by the definition of m 9 2 Preprocessing the implementation It is also necessary to preprocess the implementation Q firstly so that the events in aQ are primed as necessary and secondly so that they are renamed i e with prep defined in section 6 in preparation for the syntactic manipulation that allows the extraction function to be encoded We therefore define aA aA Q Qip and Q Q prep 9 3 Extracting traces and detecting blocking We now define a process RE for each non identity extraction pattern ep the set of which processes will be combined with Q the renaming of the implementation process for the purpose of carrying out the extraction of traces in order to extract the traces of the implementation and to convert the blocking after any trace t dom of any channel b bnia to a refusal of the event dj In the first case we give the definition of the process
27. that for i 4 j if c xW N xW then c in W and c out W or c out W and c in Wj In CSP that a process Q implements a process P is denoted by P Lx Q where X denotes the model in which we are working T denotes the traces model F the stable failures model and FD the failures divergences model P Er Q if and only if TQ C rP P Cr Q if and only if TQ C TP and oQ C oP P Crp Q if and only if Q C P and 1 Q C 1P Note that the alphabet component plays no role here It is the case that for any process term P P dP U t R t 6P A RC aP In addition we define 7 P t t R 6 P and observe that r P TP U OP where 7P is the meaning of Compositional Verification using FDR2 5 P in the traces model Finally we define mind P t t P A Vu lt t u 8P and have that TP mind P U t t R dP 15 P x denotes the semantic meaning of P in the model X T F FD while P x Q if and only if P x Q x From the above definitions of the failures divergences and stable failures models respectively it is easy to see that if P then P 6 P and 7 P 7P t t R dP We use DIV to denote the immediately diverging process and observe that DIV 7 note that we have omitted the alphabet component here 15 In FDR2 deadlock freedom is checked in the stable failures model A process P is deadlock free if and only if for every t R
28. tuple combining a number of data types In the event that the right hand event of a pair is then we can simply leave the event as it was originally However if this is not the case a pair of events have to be encoded by a single event occurring on a single channel As a result we are required to define a number of new channels with corresponding new data type extensions the new data type will represent the data values which may be sent on the original channel along with both the channel name and data type of events which may form the right hand component of a pair In general the approach to be taken will be as follows We take a channel from B on which an event occurs that forms the left hand event of a pair as described above Assume that this channel has the form chan dat where chan is the name of the channel and dat is the type of the data that it carries The event which is the right hand event of the pair will occur on channel b and we assume that this event has the form b specDat again b is the name of the channel and specDat is the type of the data that it carries Then we create a new channel called extract chan Where the name of the original channel may be derived from the subscript of the new name The data type of this new channel is dat name specDat a data tuple is defined in FDR2 using dot notation where name is a data type containing a single value namely the label of the channel b 6 If we consider the running exa
29. type of state contributes to a refusal of LCEP after t but that it contributes no more than that recall the meaning of DIV in the stable failures model In the event that b is an input channel it is relatively straightforward to generate the necessary refusal sets after t dom to generate a single maximal refusal set we simply offer the complement of a maximal set from ref t We then use the non deterministic choice operator indexed over the set of maximal sets from ref t to make sure that all of the necessary refusal sets are generated In the event that b is an output channel we wish to offer at each relevant state an event from the complement of each maximal set in ref t as a result we index the deterministic choice operator with the set of maximal sets from ref t and then use the non deterministic choice operator to pick an event from the complement of a maximal set We first give the definition of LCEP when b is an input channel In this case LCEP amp LCEP Quenest 1 gt LCEP t o a 0 DIV if t dom in A LCEP t GaeNest t gt LCEP t 0 a O DIV N if t Dom dom Drerm Oac ag ra gt DIV We now give the the definition of LCEP when b is an output channel In this case LCEP LCEP Ge neat 1 gt LCEP to a O DIV Tee dom out A
30. w such that v in Q E DoMep and v aQ v OQ It follows that v mindQ since otherwise v mindQ 3 We first observe that 6 PP PP 1 PPr PPr t R R C NotNext p t A above and the fact that Dom aB if bi bia t R t Dom A R C NotNect t and that vi T t Bi Dom The proof follows from the 5 Processes supplied to FDR2 as input must be such that they can be represented operationally by a finite variant of a labelled transition system Although generic process definitions in this and subsequent sections such as PP t may appear to be parameterized by labels from possibly infinite sets we assume that there is a finite equivalence relation over these labels such that if two processes are parameterized by equivalent labels then they are semantically equivalent In fact the concrete inputs provided to FDR2 will not be parameterized in such a way i e they will not be parameterized by a particular trace since the user will define a single distinct process name to represent the set of processes parameterized by equivalent labels 12 J Burton Corollary 4 The following hold TAO Sam 6Q C Q pi Ift TLQ TLQ then t in Q g Domep 2 If t R oQ and t inQ E Domep then t R Q If t R E dQ then there exists t X dQ such that a X CR b RN aout Q X Naout Q c RN ain Q X Nain Q C NotNest r t
31. Compositional Verification of a Network of CSP Processes using FDR2 to verify refinement in the event of interface difference Jonathan Burton Department of Computing Science University of Newcastle Newcastle upon Tyne NE1 7RU U K j i burton ncl ac uk Abstract The paper 5 presented an implementation relation formalising what it means for one process to implement another in the CSP Communicating Sequential Processes 15 framework in the event that the two processes have different interfaces An improved version of the relation appears in 6 and allows for compositional verification of a network of CSP processes The model checker FDR2 15 may be used to check CSP refinement in the event that speci fication and implementation processes have the same interface In this paper we show how to transform the problem of checking the conditions from 6 where the specification and implemen tation processes have different interfaces into one where the specification and implementation processes have the same interface This allows us to take advantage of the existing tool FDR2 and allows automatic compositional verification using the relation developed Keywords Compositional verification communicating sequential processes behaviour abstrac tion 1 Introduction We first give some motivating detail behind the implementation relation scheme presented in 6 and reproduced in section 3 before going on to describe the results p
32. PERATA acNext t gt LCEP to a D DIV N ift Dom dom ODrerm Mae aB r a gt DIV Lemma 24 The following hold of LCEP 2 6LCEP t R t Dom dom A R E RefSets t Compositional Verification using FDR2 23 3 TLCEP Dom Proof 1 The proof is immediate 2 We consider each of two cases in turn Case 1 b in P Case la t dom In this case LCEP t a o s X a Next t A s X 6LCEP t 0 a Case 1b t Dom dom In this case oLCEP t a os X a Nezt t A s X LCEP to a WUrermt R R C R Case 2 b out P Case 2a t dom In this case PLCEP t a o s X a Nezt t A s X LCEP to a Case 2b t Dom dom In this case pLCEP t a o s X a Nezt t A s X LCEP to a U Nrerm Uacagari O X a X The proof of this part follows from the above by a straightforward induction on the length of traces using the definition of Next and lemmas 22 and 23 3 We consider each of two cases in turn Case 1 b in P Case la t dom In this case we have TLCEP t U a os a Neat t A s TLCEP to a Case 1b t Dom dom In this case TLCEP t U a o s a Neat t A s TLCEP to a U a AR RM a g R Case 2 b out P Case 2a t dom In this case we
33. Q after extraction Two checks are carried out to ensure that Q meets conditions DP and DF The first is a divergence freeness check on Q obviously carried out in the failures divergences model The other check needs to ensure that T C DoMepuep However since we know by this point that 6Q we are able to simply check that TQ C Domepuep AS we will construct the processes to represent Domepuep to be divergence free we can carry out the relevant check in the traces model Rather than define a process with the traces of Domepuep and use it as the specification process in a refinement check with Q we take the following approach based on the way in which Domepuep is defined in EP6 according to each Dom As a result we carry out a refinement check for each relevant extraction pattern in turn rather than carrying out a single refinement check Note that we need only carry out the refinement check for non identity extraction patterns referring to output channels Theorem 7 Q meets conditions DP and DF if and only if 5Q and for every t TQ and every ep ep such that bi bnia t Bi E Domi Proof Since Q meets conditions DP and DF we have immediately that if t T Q and t in Q Domep then t 6Q By lemma 3 2 it follows that 6Q 0 Since 6Q 0 TQ r Q and it follows by lemma 3 3 that if t TQ then t in Domep Since Q meets condition DP it follows that if tE r then t Tei B
34. RE when b in P In this case RE REP Gren 1 gt RE to domain x O DIV if t Dom dom REPUS Orem t t gt RE t o domain x O0 DIV M ift dom Rermi xe prime aB R t gt DIV We now give the definition of the process RE when b out P In this case RE RE Gren 2 gt RE t o domain x O DIV if t Dom dom out E RE t seri t T gt RE to domain x 0 DIV N ift dom RERMi zeprime aBi R DIV We now define the composition in parallel of all of the processes RE such that b bria RE llier RE 28 J Burton Lemma 28 The following hold of RE 1 aREr prime aBnia U prep aBnia 2 bRE t R domain t E domy A extract t aBniq extr domain t A Vi DAR RefSets domain t B RA prime aB prime R 3 TRE t domain t Dom A extract t aBniq extr r domain t U t o prime a 4b bria extract t aBnia extr 1 domain t Aa aB A domain t By dom A domain t o a E Domy Proof 1 The proof follows from the fact that aRE prime aB U prep aB 2 We begin by considering each of two cases in turn Case 1 b in P Case la t Dom domi In this case we have that PRE t a 08 X a m t A s
35. The mapping RefSets Dom 2 gives the set of events which the tester process to be composed with Q may refuse after the trace t Essentially the set of sets of events returned if b is an input channel gives all possible valid refusals for a sender implementation process on the channels B after the trace t has been executed on those channels where t dom if that implementation process is to meet condition LC for the channel b Likewise the set of sets of events returned if b is an output channel gives all possible valid refusals for a receiver implementation process We define RefSets t ee AY OMA X C aB Y if b out P The reason for defining RefSets in this way is that if one composes Qi in parallel with a process with all the traces of Dom and all possible refusals defined by RefSets then the composition will deadlock if and only if Q fails to meet condition LC with respect to channel b Essentially we check to see if condition LC is met by placing Q in parallel with a process which refuses as much on the channel set B as may any valid process which meets LC and then see if the circumstances have arisen which condition LC is specifically designed to prevent i e we see if deadlock has occurred on a channel set B when behaviour over those channels is incomplete The following lemma formalises the points from the previous paragraph Lemma 21 Let b be such that bi bnia Then b is blocked at the failur
36. atisfying the following EP1 B is a non empty set of channels called sources and b is a channel called target EP2 dom is a non empty set of traces over the sources its prefix closure is denoted by Dom EP3 eztr is a strict monotonic mapping defined for traces in Dom for every t extr t is a trace over the target EP4 ref is a mapping defined for traces in Dom such that for every t Dom ref t is a non empty subset closed family of proper subsets of aB and if a aB and to a Dom then RU a ref t for all R ref t As already mentioned the mapping eztr interprets a trace over the source channels B in the implementation process in terms of a trace over a channel b in the base or specification process and defines functionally correct i e in terms of traces behaviour over those source channels by way of its domain Dom The mapping ref is used to define correct behaviour in terms of failures as it gives bounds on refusals after execution of a particular trace sequence over the source channels dom contains those traces in Dom for which the communication over B may be regarded as complete the constraint on refusals given by ref is only allowed to be violated for such traces The intuition behind this requirement is that we cannot regard as correct a situation where deadlock occurs in the implementation process when behaviour is incomplete since if regarded as correct behaviour this would imply that the specificatio
37. d information the refusal bounds as separate sets labelled with the state at which they are applied and perhaps an explicit statement of the alphabets of the various B from these the necessary inputs to FDR2 can be generated automatically This can be done by simple processsing of text files since the inputs to FDR2 are text files As an example to check condition LC if we are given a process encoding Dom along with refusal bound information we may effectively lay the template provided by process LCE P over the top of this process encoding Dom and substitute for any RM in the syntactic definition of LCEP the relevant set of sets denoting the refusal bounds The method presented in this report is currently being used to verify the correctness of asynchronous communication mechanisms ACMs see for example 16 and in particular is being used to help derive abstract specifications for such mechanisms Such specifications are useful in reasoning about systems implemented using ACMs but traditionally only exist in vague forms Since the method pre sented here is compositional we can use it to verify the correctness of a particular ACM independently of any context in which it is to be placed while still basing our notion of correctness on the fact that the meaning of a process is its meaning when placed in context This is especially relevant when as is the case with ACMs none of the behaviour of the component will be directly visible onc
38. d so the approach taken is as follows We take the event to be primed and define a new channel with the same type as the original and whose name is a concatenation of the original name and some other reserved word such as prime The new event will then occur on the new channel whilst communicating the same data value as the old event For example if we were to prime the event data 0 the result could be dataprime 0 see section 9 5 for further examples Note of course that we would not be able to use channel names containing subscripts in machine readable CSP they are used here simply for the purposes of presentation and in practice we would use something like dataprime The specification process is redefined as P using p I gt P Pipi The process PROC is then defined which will be composed in parallel with P in order to separate its states into those which contribute traces and those which contribute failures in the stable failures model PROC Dacabaa gt PROC O DIV N Qaeprime abyia gt DIV 0 Dyeary gt DIV O DIV PROC is then composed in parallel with P with the result having the renaming function m applied to it to give the process NEWSPEC This process will be used as a specification process in the refinement check used to check condition RE P amp P PROC and NEWSPEC P fm For X such that t X P for some t we define D X
39. dition LC Note that in both cases we need only check the condition with respect to channel mid We assume ep4 iS Pwice it follows that B data ack Verifying Bufimpie In this case b is an input channel Assume that Q is Bufimpie after the application of preprocessing as described in section 4 and so aQ adata U aack U aout Assume that PROC is as defined above where aB adata U aack and aQ adata U aack U aout We then have that Q Q PROC aout We then define the tester process LCEP for the extraction pattern CP eP wice in terms of two auxiliary processes LCEP x and LCEP 2 LCEP Oye o 1 data x LCEP x 0 DIV LCEP x ack yes LCEP O ack no gt LCEP x 0 DIV M Ne fadata Gye aB R Y gt DIV LCEP x data z LCEP O DIV N MrefaB data c Gye aB r Y gt DIV From these process expressions we were able to define FINALIMPLE for ep eP wice When by is an input channel and check it for deadlock freedom using FDR2 as a result of which we have checked condition LC for Bufimpie Verifying Sendimpic In this case b is an output channel Assume that Q is Sendimpie after pre processing and so a adata U aack U ain Assume that PROC is as defined above where aB adata U aack and aQ adata U aack U ain We then have that Q1 Q PROC ain We define the tester process LCEP
40. e w X if and only if there exists Z RefSets w Bi such that aB N X U Z aB Proof In what follows let t w Bi gt Let b be blocked at w X Case 1 b out P We know that aB N X ref t Therefore for every S ref t there exists a aBi N X such that a S It follows that there exists Y Off t such that Y C aB N X By definition of RefSets we know that Z RefSets t where Z aB aB N X C aB Y It follows Case 2 b in P We know that aB X ref t and so Z RefSets t where Z aB X It follows that Z U aB N X aB lt Suppose that there exists Z RefSets t such that aB N X U Z aB We therefore have that aB X C Z Case 1 b out P Z is such that Z C aB Y for some Y Off t It follows that aB X C aB Y and so Y C aB N X By definition of Off we have that aB NX ref t and so b is blocked at w X Case 2 b in P It follows by definition of RefSets t that Z ref t and so aB X ref t meaning that b is blocked at w X The next two results are used to relate the failures of the tester process defined in section 8 2 to RefSets Lemma 22 Let b in P Then Urerm iR R C R 85 S RefSets t 22 J Burton Proof The proof follows from the the definition of RefSets t and the fact that ref t is the subset closure of RM Lemma 23 Let b out P Then perm
41. e it has been placed in a system and all internal communication hidden Acknowledgements This work was supported by EPSRC studentship no 99306462 Thanks are also due to Maciej Koutny for reading numerous drafts of this report and suggesting many useful improve ments References 1 E Brinksma A Theory for the Derivation of Tests In Protocol Specification Verification and Testing VIII S Aggarwal and K Sabnani Eds North Holland 1988 63 74 2 S D Brookes C A R Hoare and A W Roscoe A Theory of Communicating Sequential Process Journal of ACM 31 1984 560 599 10 11 12 13 14 15 16 Compositional Verification using FDR2 33 S D Brookes and A W Roscoe An Improved Failures Model for Communicating Sequential Processes Proc of Seminar on Concurrency S D Brookes A W Roscoe and G Winskel Eds Springer Verlag Lecture Notes in Computer Science 197 1985 281 305 J Burton M Koutny and G Pappalardo Verifying Implementation Relations in the Event of Interface Difference Proc of FME 2001 Formal Methods for Increasing Software Productivity J N Oliveira and P Zave Eds LNCS 2021 2001 364 383 J Burton M Koutny and G Pappalardo Implementing Communicating Processes in the Event of Interface Difference Proc of ACSD 2001 Second International Conference on Application of Concurrency to System Design A Valmari and A Yakovlev Eds IEEE Computer Society 2001 87 96 J Burt
42. e of this rather than having to ensure that our modified implementation process either refuses everything on B if b is blocked or otherwise offers as much on b as is consistent with the traces of the specification we either refuse the event d if b is blocked or offer d otherwise This also means that we must prime events in the implementation in the same way as in the specification In addition we make sure that every t TP can be extended by any event d since otherwise the traces of our constructed implementation process may fail to be contained in those of our constructed specification this is because if a channel b is not blocked in Q then it is ignored by condition RE while this fact of non blocking will give rise to the occurrence of an event d in the constructed implementation process 9 1 Preprocessing the specification We first show how the specification process P must be preprocessed in order that it has the necessary semantic characterisation To do this we define two renaming relations which will be used to prime events along with one to rename primed events on either aB or ab such that bi bnia to di The relations p and prime are defined for events a such that a aB or a ab where b bnia 26 J Burton prime a a and pla a a If a prime aB or a prime ab where b dria m a dj The act of priming an event cannot be done directly in machine readable CSP an
43. e that it offers at least one event from each of the sets of events one of which must be offered in its entirety by M This guarantees that the sender M and receiver N processes remember that these notions of sender and receiver are defined here only with respect to the channel set B will synchronize on at least one event and deadlock will not arise across B Conversely if either M or N fails to meet condition LC with respect to the channel set B then deadlock may arise across B when the two processes are composed in parallel We therefore create a tester process such that if our implementation process fails to meet condition LC then deadlock will arise across the channel set B in the parallel composition of the tester and the implementation at some point where behaviour is incomplete with respect to dom Finally in order that we may transform the checking of condition LC into a check for deadlock freedom across a process as a whole we must isolate the refusals of the implementation process with respect to the channel set B This latter fact means that we check the condition for each extraction pattern in turn although once more we need not check the condition for identity extraction patterns which allows for greater compression since we hide all events not on the channels B Transforming the implementation process We now show how to transform the implementation process Q such that its failures are projected onto aB that is
44. e that Q has already successfully passed the verification checks for conditions DP and DF This allows us to derive the following results appealed to in the checking of condition TE Lemma 10 Assume that Q meets conditions DP and DF Then T TQ TDom Proof By theorem 7 56Q and so r iQ T The proof follows from lemma 3 3 and the fact that Q meets condition DP Corollary 11 Q meets condition TE if and only if ext epuep TQ ERP Remember that we assume 6P and so 7 P TP Corollary 11 allows us to check condition TE working only in the traces model and so all results and proofs in the remainder of this section assume we are working in that model By virtue of that same corollary we must generate an implementation process to be supplied as an input to a refinement check in FDR2 such that it has precisely the extracted traces of Q This means that we must generate a process context in which to place Q such that the context encodes the extraction function extr a function from traces to traces We show exactly how to do this below Intuitively the approach is similar to that employed to extract traces in the algorithms given in 4 For each extraction pattern ep we define a process TE such that in a sense each event in the alphabet of TE is a pair One of the events of the pair comes from aB i e the events from the implementation alphabet which are interpreted by ep and the other is either or
45. ec Shown in figure 1 a Send spec generates an infinite sequence of 0s or an infinite sequence of 1s depending on the signal 0 or 1 received on its input channel in at the very beginning of its execution Buf spec is a buffer process of capacity one forwarding signals received on its input channel mid In terms of CSP we have Send spec ic 0 1 mi gt S and Buf spec ic 0 1 Mid i Bi where S mid i gt S and B out i Buf spec for i 0 1 Suppose that the communication on mid is liable to fail and has therefore been implemented using two channels data and ack where data is a data channel and ack is a feedback channel used to pass acknowledgements It is assumed that a given message is sent at most twice since a re transmission always succeeds This leads to a simple protocol which can be incorporated into suitably modified original processes The resulting implementation processes shown in figure 1 b Sendimpie and Bufimpte are given by A ey Sendimpie Ueto in i gt Si Buf I gt ne ic 0 1 data i ack yes gt B N ack no gt B 6 J Burton where B S and Bi i 0 1 are auxiliary processes defined thus D II data i ack yes gt Si D ack no data i Si len gt Uieso 1 data i gt B oj A F out i gt Bufimple Suppose we wish to show that Bufimpie iS a valid implementation of Bufspec We need
46. ee the example below in section 6 2 We have 7 t a t a E Next t where a if extr t extr t o a i a t a extract chan data b val if extr t o e extr t0 a where a chan data and e 0 val Observe that A a t simply returns a if the extraction of t is identical to the extraction of t o a In this case the relevant event pair in r TE would have a as the left hand component and as the right hand component In the other case namely that the extraction of t is a strict prefix of the extraction of t o a we are effectively encoding the fact that a is the left hand component of the event pair and e is the right hand component We now give a lemma which formalises the fact that 7 TE domain Dom and 7 TE extract aB extr Dom Lemma 12 The following results hold 1 If w TTE then domain w Dom 2 Ift Dom there exists w TTE such that domain w t 3 If w E TTE then extract w aB extr domain w Proof 1 The proof is a straightforward induction on the length of w using the definitions of m and domaini 2 The proof in this case is a straightforward induction on the length of t using the definitions of m and domaini 3 The proof is once more a straightforward induction on the length of w this time using the definitions of m domain and eztract In addition extr domain w is well defined by part 1 of the lemma
47. efines various syntactic terms which are used either directly or as components in larger terms to define the inputs supplied to FDR2 Where appropriate the example given in this section is used to provide a concrete example of how those syntactic terms would be used in practice this gives both an illustration of the method at work and also allows us to verify automatically and compositionally that Sendspec D Bufspec EFD Sendimple D Bufimpie Although we will define such syntactic terms using the standard CSP syntax all of the operators used have a direct equivalent in the machine readable syntax Also as a final point it is worth noting that the immediately diverging process does not have a distinguished syntactic representation in the way that for example the immediately deadlocking process does i e STOP As a result we define the auxiliary process X a X and define the immediately diverging process DIV X a 4 Preprocessing the implementation process Note that throughout this section we work within the full failures divergences model Since none of the various components of the implementation relation we are to verify are interested in traces which when projected on the input channels of Q are not found in the set of valid traces over the input channels as defined by Domep it is necessary to remove them before proceeding with the verification proper For example imagine that t E TQ but t in Dome Condition DP p
48. es mid 1 prep lt data 0 data 0 data 1 data 1 ack no ack no data 0 extractgata 0 mid 0 data 1 extractgata 1 mid 1 extractac yes mid 0 mid 0 extractack yes mid 1 mid 1 extract 4 extractaaia 0 mid 0 mid 0 extractgata 1 mid 1 mid 1 Note that here extract extract and Byiq B Using the process expressions defined here we were able to define INTERP as above and verify automatically using FDR2 that Bufimpie meets condition TE with respect to Bufspec 7 Checking condition GE The condition to be checked is GE If t is an w sequence in Tp9mQ then extr epuep ti is also an w sequence Once again we assume that we have successfully verified conditions DP and DF Checking condition GE simply requires that we check INTERP for divergence freeness and so obviously we work in the failures divergences model Lemma 18 6TE where TE is as defined in section 6 Proof We first have that 6TE for i I since neither the deterministic choice operator nor the prefix operator can introduce divergence The proof then follows from the above and the fact that the parallel composition operator cannot introduce divergence Theorem 19 Q meets condition GE if and only if INTERP 9 Proof In what follows we extend the renaming relations domain and extract and the mapping extr to infinite traces in the usual way Remember that we assume our input processes are finite
49. for refusals on channels b bnia if b is not blocked in Q we need to make sure that our abstracted implementation process refuses as little as the specification might refuse on b after any particular trace This means that the abstracted implementation process needs to offer all events which are valid extensions according to TP of the extracted trace which brought us to this point in the abstracted implementation To do this would be rather difficult and there is a much easier way to proceed which is taken here We first modify the specification process P yielding P using the approach of section 8 of combining DIV with the non deterministic choice operator to give two types of state one to give the traces of the new process P and the other to give the failures At each state contributing to the failures of the process we simply need to know whether or not everything is refused on any channel b such that bi bnia We therefore rename any event offered on such a b to a distinguished event d We define dr d i I As a result rather than offering or refusing events on b the process simply refuses or accepts the event d However in order for this renaming to d to be carried out without interfering with the events which contribute to the traces of the new specification process the events from ab which give the refusals of the specification are primed and it is these primed events which are renamed As a consequenc
50. g the detail above NEWSPEC could be constructed for both Bufspec and Sendspec In the definition of RE in section 9 3 a choice operator is indexed by R RM and then a subsequent choice operator is indexed by x prime aB R In practice as shown below we actually index the first operator by prime R such that R RM and the subsequent choice operator is indexed by x prime aB R This is not important as the two ways of proceeding are equivalent the former is used in definitions for ease of expression whilst the latter is used in practice since in machine readable CSP we cannot actually apply the renaming operator to a set which is being used to index a choice operator Below let X adck prime U dataprime O and Y 4 aackyrime U dataprime 1 Verifying Bufimpic In this case b is an input channel and RE for the extraction pattern ep eP twice is defined in terms of two auxiliary processes RF x and REY 2 RE Oyeqo 1 data x gt RE x 0 DIV N Nretx y yE adata prime Waack prime R Y gt DIV RE x ertractacy yes mid c gt RE O ack no gt RE x O DIV RE x extractdata mid x gt RE O DIV Verifying Sendimpic In this case b is an output channel and RE for the extraction pattern ep eP wice iS defined in terms of the following two auxiliary processes RE x and REY x 32 J Burton RE
51. hat the implementation relation itself and so condition RE is defined in the failures divergences model According to this condition there are three major things which we need to do to the implementation process we need to extract its traces identify in some way the channels that are blocked and finally preserve refusals on channels which are uninterpreted As before we will convert blocking of a channel bi into a local deadlock on channel set B This time however we cannot isolate the refusals on B and the resulting deadlock will remain local i e it will be a deadlock across a restricted channel set rather than a deadlock of a process as a whole Processes similar to the LCEP defined in section 8 will be used to convert blocking of channels in P into local deadlock across channel sets in Q although there are two main differences The first is that the new processes defined here incorporate the features necessary to extract the traces of Q to do this they use the approach of section 6 and the processes TE The second difference is to do with making sure that too much is not refused if a channel b is not blocked The following should explain this a little more We are transforming the process Q so that it is expressed at the level of abstraction of the specification process P and wish the resulting abstracted process to refine P in the stable failures model if and only if Q meets condition RE Since RE stipulates no requirements
52. his transformation due to the fact that PQ 61Q that is we do not lose any information on failures by only working in the stable failures model The means used to check condition LC is derived directly from the rationale behind the condition and is similar in some respects to the use of tester processes in 1 where the question of whether one process implements another is transformed into a question of deadlock freedom of the implementation composed in parallel with the tester process We first explain what it means that condition LC is met by a process or processes If we take two implementation processes M and N which meet condition LC with respect to a channel b and compose them in parallel on the channel set B then at any state reachable in the resulting composed process by a trace t such that t Bi Z dom at least one event from B will be synchronized upon and so enabled meaning that deadlock will not result on that channel set This is achieved in the following way A set of refusal bounds are defined for the process M which is notionally a sender process with respect to the channels B When behaviour over the channels B is incomplete then the events refused by M must be contained within one of a set of refusal bounds the ref component of the extraction pattern ep Or to put it another way there are sets of events to be offered and M must offer all the events in at least one of the sets The receiver process N must then guarante
53. hose i th element is a and whose length t is n touis the trace obtained by appending u to t A is the set of all traces of actions from A including the empty trace A is the set of all infinite traces of actions from A T is the set of all traces t t o o tn n gt 0 such that t1 t ET lt denotes the prefix relation on traces and t lt u if t lt u and t u Pref T u 3tET u lt t if the prefiz closure of T T is prefix closed if T Pref T t b b is a trace obtained from t by replacing each action b v by b v t B is obtained by deleting from t all the actions that do not occur on the channels in B for example b 3 b 1 b 2 0 3 b 3 b 6 b 2 b b 0 1 0 3 b 3 b 2 t A is obtained by deleting from t all the actions that do not appear in A An infinite sequence t t2 is an w sequence if t lt t2 lt and limj_ 4 t co A mapping f T T is monotonic if t u T and t lt u implies f t lt f u f is strict if T and f and f is a homomorphism if t u tou T implies f t ou f t o f u A family of sets is subset closed if Y C X X implies Y X 2 2 CSP operators We now give a brief description of the CSP operators which we shall use We use deterministic choice P Q non deterministic choice PM Q and prefixing a P Parallel composition P Q models syn
54. if t R E dQ then t Bi RN aB is 20 J Burton a failure of the transformed process Since we may work in the stable failures model we are able to use the process DIV the immediately diverging process to obscure failures in which we are not interested without adding behaviours to the resulting process We are able to do this in the following way Let P be a process expression Then P O DIV t R P t That this is the case follows from the definition of O in the stable failures model and the fact that the meaning of DIV in this model is the alphabet component is omitted here In particular we are able to obscure failures derived from states where behaviour is complete over the channel set B since condition LC places no restriction on what may be refused in those situations This aproach of working in the stable failures model and crucially using DIV is also used in the checking of condition RE The following process PROC is such that after any trace we may non deterministically arrive at a state which offers all events in aQ but which does not contribute to a failure of PROC due to the appearance of DIV in that state Alternatively we may arrive at a state which offers all events in aB and then takes us to a state that is simply immediately divergent whichever event from aB we follow PROC a PROC 0 DIV N Gaeap a gt DIV
55. in which it is expressible since this simplifies proofs and the tool FDR2 is more efficient when used with simpler models 15 In the rest of this paper we deal with specification and implementation processes along with pro cesses defined to facilitate refinement checking using FDR2 If W is either a specification or implemen tation process we associate with W a set of communication channels and denote this set xW xW may be partitioned into input channels in W and output channels out W We identify the alphabet of such a process W with the alphabet of xW and stipulate that aW Uye xW ab As a result the alphabet of such a process W is taken as a given while the alphabet of any other process may be derived compositionally according to the rules in section A in the appendix These two ways of deriving the alphabet of a process are not inconsistent process alphabets are only used to calculate the semantics of processes defined using the parallel composition operator and in FDR2 we can effectively give a process any alphabet we want when using the parallel composition operator see below Processes W14 Wn form a network if no channel is shared by more than two W s We define W W to be the process obtained by taking the parallel composition of the processes and then hiding all interprocess communication i e the process W1 Wn aB where B is the set of channels shared by at least two different processes W Note
56. ions of the implementation relation are checked Finally we give some concluding remarks in section 10 2 Preliminaries In this section we first recall those parts of the CSP theory which are needed throughout the paper 2 1 Actions and traces Communicating Sequential Processes CSP 2 3 10 15 is a formal model for the description of concur rent computing systems A CSP process can be regarded as a black box which may engage in interaction with its environment Atomic instances of this interaction are called actions and must be elements of the alphabet of the process The alphabet of a process P is denoted aP A trace of the process is a finite sequence of actions that a process can be observed to engage in In this report structured actions of the form b v will be used where v is a message and b is a communication channel b v is said to occur at b and to cause v be exchanged between processes communicating over b For every channel b ub is the message set of b the set of all v such that b v is a valid action We define ab b v v ub to be the alphabet of channel b It is assumed that ub is always finite and non empty For a set of channels B aB User ab The following notation is similar to that of 10 below t u t1 t2 are traces b b b are channels B Bn B are disjoint sets of channels a is an action A is a set of actions and T T are non empty sets of traces t ay y is the trace w
57. is by ensuring that progress will not be possible on the 1 In general Dom Pref dom meaning that each interpretable trace has at least in theory a chance of being completed 2 In general we will only be interested in traces belonging to Dom 3 We are able to work only in the stable failures model since we assume the divergence freeness of any specifi cation component and also with a slight qualification require the divergence freeness of the implementation component Compositional Verification using FDR2 7 corresponding channel in the specification component Here lack of progress on internal channels leads to the fact that the relevant state will give rise to a failure of Pyet Finally it should be stressed that ref t gives a refusal bound on the sender side more precisely the process which implements the sender specification process But this is enough since if we want to rule out a deadlock in communication between the sender and receiver on a localised set of channels it is now possible to stipulate on the receiver side that no refusal is such that when combined with any refusal allowed by ref t on the sender side it can yield the whole alphabet of the channels used for transmission 3 2 Formal definition The notion of extraction pattern relates behaviour on a set of channels in an implementation process to that on a channel in a specification process An extraction pattern is a tuple ep B b dom extr ref s
58. is used here is FDR2 13 15 developed for the purposes of model checking CSP As implied above FDR2 takes as input two processes one a specification and the other an implementation which must have the same interface The implementation relation described in section 3 takes as input a specification process and an implementation process with possibly different interfaces along with a means of interpretation called extraction patterns and described in section 3 which acts as a parameter to the relation We show here how to transform this set of inputs into a set of inputs acceptable to FDR2 using only the syntatic operators of the CSP language such that a set of refinement checks within FDR2 are successful if and only if the conditions from the implementation relation are met This then gives automatic compositional verification of a network of CSP processes It turns out there are a number of different ways in which this problem may be approached the most fundamental distinction perhaps being whether we choose to work at the level of abstraction of the implementation process or at that of the specification process For we must transform syntactically one of the processes so that it has the same interface as the other it is this transformation which allows us to use FDR2 It seems that different approaches may work better in different contexts For example working at the level of abstraction of the specification means that we can make the in
59. laces no restrictions on and in subsequent conditions we take no notice of it since we only interest ourselves in traces in TpomQ However if we do not remove such traces from our implementation process they will remain when we Compositional Verification using FDR2 II come to carry out refinement checks using FDR2 and may cause a particular refinement check to fail despite the fact that the relevant condition has been met a As a result we remove these traces from Q creating a process Q such that t E TQAt in Q E Domep if and only if t rQ we refer here to TQ rather than 7 Q since we are not interested in traces which are only present due to the presence of divergence Although this preprocessing affects the failures of Q it does not do so in such a way that the answer to the verification question is different for Q than it is for Q see theorem 6 In order to carry out this preprocessing on Q we simply compose it in parallel with a component process for each of the extraction patterns which deal with an interpreted input channel i e the ex traction pattern is not an identity extraction pattern Each of these processes is capable of performing exactly the traces from the Dom component associated with the relevant extraction pattern Note that it is unnecessary to include identity extraction patterns in our preprocessing since Dom for such an extraction pattern ep simply allows the execution of any trace over abi We fi
60. llows let P and Q be CSP process terms that is syntactic definitions of CSP processes Note that the word process may denote either a syntactic term or a semantic object In what follows the description process will be suitably qualified where the context requires it The simplest model of behaviour in CSP is the traces model where a process term P is modelled by a pair aP TP TP or the traces of P is the set of finite sequences of visible actions which that process may execute In the stable failures model a process term P is modelled by a triple aP TP P where P the stable failures of P is a subset of aP x 2 If t R P then P is able to refuse R after t Intuitively this means that if the environment only offers R as a set of possible events to be executed after t then P can deadlock when placed in parallel with the environment In the failures divergences model a process term P is modelled as a triple aP 1 P P where 6P divergences is a subset of aP and P failures is a subset of aP x 2 P Ift P then P is said to diverge after t In the CSP model this means the process behaves in a totally uncontrollable way Such a semantical treatment is based on what is often referred to as catastrophic divergence whereby the process in a diverging state is modelled as being able to accept any trace and generate any refusal When verifying a given property we shall always use the simplest model
61. locked at a failure t R in Q if either b is an input channel and aB R ref t Bi or b is an output channel and aB N R ref t Bi blocking is not defined for any channel c bia Note that in both cases this signifies that the refusal bound imposed by the ref has been breached We then call Q an implementation of P w r t extraction patterns ep and ep denoted Q lt P if the following six conditions are satisfied DP Ift Er Q is such that t in Q Dome then t E TpomQ DF TpomQN Q TE ertr epuep TDomQ C T1 P GE If t is an w sequence in TpomQ then ettrepuep ti is also an w sequence LC If brig and b is a channel of P blocked at t R E pomQ then t Bi dom RE If t R E ddomQ then ertr epuep t vB U RN abia 1 P where B C bria is the set of all channels of P blocked at t R We interpret the above conditions in the following way DP expresses the domain preservation prop erty which says that if a trace of Q projected on the input channels can be interpreted by ep then it must be possible to interpret the projection on the output channels by ep Note that such a condition is a simple rely guarantee property in the sense of 8 DF can be interpreted as divergence freedom within the domain of Q recall that CSP divergences signify totally unacceptable behaviour TE simply states that within the domain of Q we insist on generating P s traces af
62. mple and ep introduced in section 3 the trace data 0 ack yes extracts to mid 0 where b is the channel mid If it were possible to use the notion of event pairs directly we could encode this using the trace data 0 ack yes mid 0 Since we cannot use such pairs directly in the representation of the extraction pattern this trace would become data 0 extractack yes mid 0 Notice that data 0 remains as the original event since the right hand component of the pair of which it was the left hand component is simply As another example consider the trace data 0 ack no data 0 also extracting to mid 0 In this case using event pairs we would have data 0 ack no data 0 mid 0 In the extraction pattern representation the trace would be come data 0 ack no extractdata 0 mid 0 Note that we have both an occurrence of the unchanged data 0 and also an occurrence of data 0 modified to allow the extraction function to be encoded Note also that in machine readable CSP we cannot have channel names containing subscripts we use the device here for the purposes of presentation and in practice would have to define channels such as for example extractchan or extractdata Renaming functions We now give the renaming functions which can be used to reclaim Dom and extr Dom respectively from 7TE The renaming domain will return Dom and extract will return eatr Dom The functions domain and extract are both
63. n process could in some sense deadlock while in the middle of executing a single atomic action The extraction mapping is monotonic as receiving more information cannot decrease the current knowledge about the transmission aB ref t will be useful in that for an unfinished communication t we do not allow the sender to refuse all possible transmission The second condition in EP4 is a rendering in terms of extraction patterns of a condition imposed on CSP processes that impossible events can always be refused see SF4 and FD3 in section A in the appendix We note that not all channels require all components of an extraction pattern to interpret their be haviour We shall denote these channels uninterpreted or identity channels and their extraction patterns identity extraction patterns Intuitively these channels have the same interface in both implementa tion and specification In particular all channels which remain visible in the final compositions of the implementation and specification components respectively for example Qyez and Pyet are of this type For an extraction pattern ep let b c be an uninterpreted channel Then B c and Dom dom ac If t Dom then extr t t That is the extraction mapping for such channels is the identity mapping i e behaviour over them does not require further interpretation Finally no ref component is specified for such an extraction pattern 4 For the purposes of this report we a
64. n the specification process the refusal of all communication on the corresponding channel and moreover the trace t itself is complete i e t dom For example in the process described above if Sendimpie has just communicated data v then its behaviour cannot be complete and so it cannot refuse anything on the channel ack i e it must be ready to receive either a positive or a negative acknowledgement And if behaviour is complete ie t dom in Bufimpie it can for example refuse an event on channel data only if Bufspec can refuse everything on channel mid after performing extr t The refusal bounds given by ref may be thought of as ensuring a kind of liveness or progress condition on sets of channels upon which composition will occur when implementation components are composed to build a full implementation system Qye introduced in section 1 Since these channels are to be composed upon and so hidden the progress enforced manifests itself in the final system as the occurrence of an invisible transition and states in which an invisible transition is enabled do not contribute a stable failure of Q yet Conversely if we may not enforce progress after a complete behaviour then it is possible that the relevant state reached will contribute to a failure t R of Qnez Since in the stable failures model of CSP if Quet implements Pyet then Qnet C Pyet we must ensure that the relevant failure t R also occurs in Pyet We do th
65. of this part follows from the above the definition of m and the semantic definition of the renaming operator see section A in the appendix and recall that m d prime ab U prime aB 3 We first observe that TQ t p t TQ From this we have that rQ t p domain t TQ From the above the fact that the extraction mapping is the identity mapping if ep is such that bi brig and lemma 28 3 we have that T Q REr t domain t TQ A extract t aBnia ext epuep domain t U t o prime a Ew o a TQ bi bnia domain t w A extract t aBnia extr epuep w Aa eaB w B dom 30 J Burton From the above we have that _ TPREIMPLE eztr epuep TQ U t o prime a Gw o a TQ bi bnia ext epuep w t Aa EaBi A wl Bi dom The proof of this part follows from the above Note from the above result that if t R FINALIMPLE then t extr epuep w for some trace w of Q such that w domepuep This is because due to the definition of condition RE we are not interested in what is refused in Q after traces which are not complete We now give the final result which lets us check condition RE using FDR2 Theorem 30 Q meets condition RE if and only if NEWSPEC Cp FINALIMPLE Proof gt We assume that Q has been shown to meet condition RE and prove that NEWSPEC Cp FINALIMPLE under this assumption Since we
66. om Proof 1 We observe that aQ aQ U prime aBnia from which we have that aQ abia U prime aBnia U prep aBnia From this and lemma 28 1 we have that a Q REr abia U prime aBnia U prep aBnia From the above and by definition of extract we have that aPREIMPLE aP U prime aBnia The proof of this part follows from the above by definition of m 2 We first observe that pQ t R A w X 1Q p t w A RC XU prime X NaByia remember that 6Q 1Q since 6Q We then have that p t R lw X 61 0 p domain t w ARC X Nabia U prime X NaBnia U prep X N aBnia From the above the fact that the extraction mapping is the identity mapping and dom ab if ep is such that b bnia and lemma 28 2 we have that PC REr t R Glw X 91 Z C aBnia domain t w domepuep A extract t aBnia extr epuep w A Vi I ZN aB RefSets w Bi ARC XN abia U prime X N aBnia U prep aBnia U prime Z From the above and by definition of extract we have that PREIMPLE t R A w X 1 9 Z C aBnia w E domepuep At extr epuep w A Wi I ZN aB RefSets w Bi ARC X Nabia U prime X N aBnia U abnia U prime Z By lemma 21 and the definition of prime we have that if bi bnia bi is blocked at w X if and only if there exists Z RefSets w Bi such that prime X N aB U prime Z prime aB The proof
67. on M Koutny and G Pappalardo Compositional Verification of a Network of CSP Processes Tech nical Report 757 Dept of Computing Science University of Newcastle upon Tyne 2002 FDR2 User Manual Available at http www formal demon co uk fdr2manual fdr2manual_toc html P Collette and C B Jones Enhancing the Tractability of Rely Guarantee Specifications in the Development of Interfering Operations Technical Report CUMCS 95 10 3 Department of Computing Science Manchester University 1995 M C B Hennessy Algebraic Theory of Processes MIT Press 1988 C A R Hoare Communicating Sequential Processes Prentice Hall 1985 M Koutny L Mancini and G Pappalardo Two Implementation Relations and the Correctness of Commu nicated Replicated Processing Formal Aspects of Computing 9 1997 119 148 R Milner Communication and Concurrency Prentice Hall 1989 A W Roscoe Model Checking CSP In A Classical Mind Essays in Honour of C A R Hoare Prentice Hall 1994 353 378 A W Roscoe P H B Gardiner M H Goldsmith J R Hulance D M Jackson and J B Scattergood Hierarchical Compression for Model checking CSP or How to Check 107 Dining Philosophers for Dead lock Proc of Workshop on Tools and Algorithms for The Construction and Analysis of Systems TACAS U H Engberg K G Larsen and A Skou Eds BRICS Notes Series NS 95 2 1995 187 200 A W Roscoe The Theory and Practice of Concurrency Prentice Hall 1998
68. ow how the results given above can be used to define inputs to FDR2 to verify automatically that Bufimpie respectively Sendimpic meets condition RE with respect to Bufspec respectively Sendspec In both cases let ep be ePiyice This is the only non identity extraction pattern and d d1 Also Bnia B data ack We define new channels dataprime aCkprime and Midprime with the same types as data ack and mid respectively on which will occur the primed events Note that in the definition of PROC which is the same whichever of the two processes we are checking here the deter ministic choice operator is indexed by x prime amid although in this syntactic definition the set of events is given and then primed in practice we would index the operator directly with x amid prime to give an equivalent effect The renaming prime is defined as prime mid 0 Mid prime 0 mid 1 Mid prime 1 data 0 dataprime 0 data 1 dataprime 1 ack yes ackprime yes ack no ack prime No The renaming p is defined as p mid 0 mid 0 mid 0 Mid prime 0 mid 1 mid 1 mid 1 Mid prime 1 data 0 data 0 data 0 data prime 0 data 1 data 1 data 1 dataprime 1 ack yes ack yes ack yes ack prime yes ack no ack no ack no ack prime no The renaming m is defined as m mid prime 0 d1 Mid prime 1 d1 dataprime 0 d1 datdprime 1 d1 ACK prime Yes d ack prime no di Usin
69. partial defined only for those events which have a non empty right hand component In what follows we assume that x has the form es tract chan data b val where data and val are specific instances of data values moreover chan B The type of extract is extract aT E ab and it is defined as eztract x j val The type of domain is domain aT E aB and it is defined as domain x chan data Note that these functions are defined only for values of the form of x and not for values in aB However as with all relations we assume that partial functions are extended by the identity mapping for all elements of the domain for which the function is undefined Defining TE For each ep such that b E bniq we encode the extraction function as a process TE where TE TE and TE t Ooen t gt TE t o domain a 6 Note that the textual representations of the channel name b as a value of type name and as a channel identifier are the same whenever the label is used in what follows the type of value which it denotes will be clear from the context 7 Although in the general case we use renaming relations it happens that these are functions 16 J Burton For ease of expression the function 7 is used here to encode the modifications that must be made to the events of aB although its effects must be implemented directly in any input supplied to FDR2 since it cannot be encoded as such in CSP s
70. positional verification Yet in deriving an implementation from a specification we will often wish to implement abstract high level interface actions at a lower level of detail and in a more concrete manner For example the channel connecting P to another component process P may be unreliable and so it may need to be replaced by a data channel and an acknowledgement channel Or P itself may be liable to fail and so its 2 J Burton behaviour may need to be replicated with each new component having its own communication channels to avoid a single channel becoming a bottleneck Or it may simply be the case that a high level action of P has been rendered in a more concrete and so more implementable form As a result the interface of an implementation process may end up being expressed at a lower and so different level of abstraction to that of the corresponding specification process In the process algebraic context where our interest lies only in observable behaviour this means that verification of correctness must be able to deal with the case that the implementation and specification processes have different interfaces The relation between processes detailed in 6 and given in section 3 enjoys two crucial properties that allow us to carry out compositional verification in the event that Q and P have different interfaces The first is that of compositionality meaning that the implementation relation distributes over system composition Th
71. process as in figure 2 and ep Bi bi dom extr ref be an extraction pattern for every i lt m n We assume that the B s are mutually disjoint channel sets and denote ep P1 Dm and ep epm41 Pm4n We then take a process Q such that in Q B U UBm Compositional Verification using FDR2 9 b gt gt bm 1 B gt Bm 1 Q bm LC bmtn Bm H Bmin Fig 2 Base process P and its implementation Q and out Q Bm 1U U Bm n as shown in figure 2 and denote by TpomQ the set of all t T1 Q which belong to Domepuep Similarly PpomQ and pdomQ will be the sets of those failures in 1Q in which the trace component belongs to Domepuep and domepuep respectively Intuitively Tpom which is subsequently referred to as the domain of Q is the set of t T Q which are of actual interest and consequently dpomQ is the set of t R 1Q of actual interest too In what follows we denote the uninterpreted channels of P as biq Note that these are also the uninterpreted channels of Q The interpreted channels of P are denoted briq and the interpreted channels of Q are denoted Bnia This means that aQ aBnia U abiq and aP abnig U abjg We define also I i bi bnia intuitively J means interpreted and then ep ep i I We then write extry for extrep Dom for Domep and so on We will say that a channel b of P is b
72. puts supplied to FDR2 as small as possible which allows us to verify larger processes However this can cause problems when we approach debugging since all counter examples are generated at this higher level of abstraction and it is more difficult to relate them to the behaviours of the implementation In the future it is likely that different approaches will be implemented and a choice will be made between them by the user as appropriate For the momement however in the absence of the necessary experimental data the rationale followed in this report has been to make the inputs to FDR2 as small as possible this is because reducing the size of processes seems unlikely to lead to significant if any slowdown while allowing us to work with a greater range of possibly quite large examples The remainder of the paper is organised as follows In the next section we present some preliminary definitions In section 3 we describe the device of extraction patterns introduce the implementation relation and give the results which allow us to use it for the purposes of compositional verification Compositional Verification using FDR2 3 Section 3 also introduces a running example which will be used to illustrate how the verification method works in practice Section 4 describes the preprocessing which must be carried out on an implementation process before verification can begin and the subsequent sections detail the manner in which the indi vidual condit
73. resented in this paper Consider the situation that we have a specification network Pyet composed of n processes P where all interprocess communication is hidden Consider an implementation network Q Net also composed of n processes again with all interprocess communication hidden Assume that there is a one to one correspondence between component processes in Pye and those in Que Intuitively P is intended to specify Q Finally assume that the interface of Q yet in terms of externally observable actions is the same as that of Pyet In process algebras such as those used in 12 15 the notion that a process Qyet implements a process Pyer is based on the idea that Q yet is more deterministic than or equivalent to Pyet in terms of the chosen semantics We then say that the behaviour of Quet refines the behaviour of Pyet Moreover the interface of Qnez the implementation process must be the same as that of Pyet the specification process to facilitate comparison What if we wish to approach this verification question compositionally What if we want to verify that Qnet implements Pyet simply by verifying that Q implements P for each 1 lt i lt n In general this is only possible if Q and P have the same communication interface Thus Q may implement P by describing its internal and so hidden computation in a more concrete manner but it may not do so by refining its external interface at least if we wish to carry out com
74. roof By lemma 12 3 extract w aTE aB extr domain w aTE for each i I By definition of a TE and domain we observe that domain aTE aB From the fact that domain and domain have disjoint ranges for i 4 j we then have domain w aTE domain w domain aTE domain w aB t aB It follows that extract w aTE aB extr t aB Moreover for all 1 lt j lt m n such that j I i e bj big we know that eztr w aB w aB by definition of the extraction mapping for uninterpreted channels and also that eztract w aBnia aB w aB The proof follows from the above and EP7 We are now able to give the final theorem showing how we may check condition TE using FDR2 Theorem 17 Q meets condition TE if and only if P Cr INTERP Proof By corollary 11 we need only prove that ext epuep TQ C TP if and only if P Er INTERP gt Assume that eztr epuep TQ C 7P Let t rINTERP Then there exists w r Q prep TEr such that extract w aBnia t By lemma 15 we have that domain w u TQ By lemma 16 t extr epuep u It follows that t rP and so P Er INTERP lt Assume that P Er INTERP Let t rQ By lemma 15 we know there exists w 7 Q prep TE such that domain w t By lemma 16 we know that eztract w ABniq estr epuep t and so ettrepuep t E TINTERP Since P Er INTERP we have that eztrepuep t TP and so ext
75. rst define a mapping Nezt Dom 2 such that Nezt t a to a Dom This mapping is used throughout the report and gives the possible extensions to a trace such that the resulting trace remains a member of the domain Dom We also define the complement of Next as NotNezt where NotNezt Dom 27 and NotNest t a to a g Dom Let I i ep ep A bi bnia We then define NotNeztr U er NotNeat We then have that PP PP and PPi t Dac nern ea gt PPi t o a where PP is a component process to be composed in parallel with Q during preprocessing We finally define PPr lier PP and Q Q PPr where Q is Q after preprocessing has been applied Lemma 3 The following hold of Q ds a aQ 2 6Q tou t E mindQ A t in Q E Dome u aQ 3 19 Q U t R t dQ where 6Q t R A t X Q Y C NotNeztr t t inQ Dome A RCXUY Proof 1 The proof is immediate since aPPr U paBi C aQ we assume that if a process can execute exactly the traces of Dom then its alphabet is aB 2 We first observe that 6PP and so 6PPr The proof follows from the above the fact that t B Dom is met trivially if ep is an identity extraction pattern and the divergence semantics of the parallel composition operator With respect to the latter note that since PPr 0 and aPPr C aQ if w Q there exists v mindQ v lt
76. s violated in Q We then have that t R Q By corollary 4 4 we have that t R 4Q and so t R PDom t R baom As a result condition LC RE would be violated at t R in Q and so we have a contradiction Compositional Verification using FDR2 13 As a result of the above theorem we are able to verify that Q is a valid implementation of P according to the scheme presented here by instead verifying that Qi is a valid implementation of P Although in the proofs above we have assumed that all of the PP are composed in parallel before being combined with Q to generate Q in practice we would compose each PP with Q in turn which is possible due to the associativity of the parallel composition operator This is desirable since it avoids the state explosion which might result from composing the disjoint PP in parallel first 5 Checking conditions DP and DF We are now in a position to begin checking the first two conditions DP and DF which are as follows according to theorem 6 we may substitute Q for Q DF Q N TDomQ 0 DP Ifte7 Q and t in E Dom then t E TpomQ Although the checking of subsequent conditions will allow us to abstract the behaviour of Q and interpret it in terms of the interface of the specification process P conditions DP and DF are checked at the level of abstraction at which Q is expressed Condition LC is similar since it too makes no reference to the behaviour of
77. ssume that eztr t o a lt extr t 1 8 J Burton Twice extraction pattern For the example given here in order to demonstrate that Sendimple and Bufimple are implementations of respectively Sendspec and Bufspec we will need an extraction pattern eP twice We also observe that the channels in and out are uninterpreted For the eP wice extraction pattern B data ack are the source channels and b mid is the target channel moreover umid udata 0 1 and pack yes no The remaining components of ep jnice are defined in the following way where t dom and tou Dom dom data 0 ack yes data 0 ack no data 0 data 1 ack yes data 1 ack no data 1 iftou extr tow amp q SND mies aed F extr t if u data v or u data v ack no zadati if u data v ref tou lt R e Qxdetavaack adata Z R ifu R e Qedatavaack data y g R if u data v ack no Here intuitively we can extract mid 0 from two sequences of communications data 0 ack yes and data 0 ack no data 0 and similarly for mid 1 A valid trace in Dom is one which is a concatenation of a series of complete segments of this kind possibly followed by an initial fragment of one of them Any trace for which the latter is true is incomplete and belongs to Dom dom otherwise it belongs to dom 3 3 Additional notations The various components of the extraction patterns can be annotated e g subscripted to
78. ter extraction GE states that an unboundedly growing sequence of traces in the domain of Q is a sequence of traces unboundedly growing after extraction notice that we place no restriction on the relative growth of the w sequences ti and extr epuep ti LC means that going outside the bounds of allowed refusals indicates that the communication on a given interpreted channel may be considered as locally completed Finally RE states a condition for refusal extraction which means that if a trace is locally completed on all channels any local blocking of an interpreted channel of P in Q is transformed into the refusal of its whole alphabet in P moreover the refusals on the uninterpreted channels in Q should be matched in P A direct comparison of an implementation process Q with the corresponding base process P is only possible if there is no difference in the communication interfaces This corresponds to the situation that all of the channels of Q and of P are uninterpreted In such a case we simply denote Q lt P and then we can attempt to directly compare the semantics of the two processes in question Theorem 1 If Q lt P then P Erp Q i e Q C OP and 61Q C P N B The latter implies that T Q C T P as it suffices to take R 90 10 J Burton The next result states that the implementation relation is compositional in the sense that it is preserved by the network composition operation Taken with the previous res
79. ult we have met both of the restrictions stated in section 1 and so have a means of compositional verification in the event that corresponding specification and implementation component processes have different interfaces Theorem 2 Let K and L be two base processes whose composition is non diverging as in figure 3 and let c d e f g and h be sets of extraction patterns whose targets are respectively the channel sets C D E F G and H If M lt Q K and N lt i f L then MON lt D KOL E F t t f D C K he L G 2H Fig 3 Base processes used in the formulation of the compositionality theorem Hence the implementation relation is preserved through network composition and the only restriction is that the network of the base processes should be designed in a divergence free way This means of course that the base processes themselves must be divergence free and so we assume 6P for the base process P described above However this is a standard requirement in the CSP approach recall again that divergences are regarded as totally unacceptable 3 5 Remainder of the report Each of the subsequent sections deals with checking the conditions of the implementation relation given here showing how this can be carried out using a standard notion of what it means for one process to implement another in CSP As a result this allows us to use FDR2 to verify the implementation relation Each section d
80. us a specification composed of a number of connected systems may be implemented by connecting their respective implementations and so we may verify compositionally that Q yet implements Pyet according to our implementation relation scheme simply by verifying that each Q implements P Moreover although in general Q and P do not have the same interface we know that when all of the components Q have been composed the result namely Qyez will have the same interface as the corresponding specification process namely Pyet By the compositionality property we know that Q wnet implements Pyet according to the scheme presented here We then impose the requirement that the implementation relation presented here reduces to a standard notion of behaviour refinement in the CSP framework in the event that the implementation and specification processes have the same interface This allows us to verify compositionally that Q wnet implements Pyet In order to apply the implementation relation described above to non trivial examples it is necessary that we have some means for its automatic verification The approach taken in this paper is to transform the verification question presented here into one which may be answered by an existing industrial strength tool In a sense we create a new tool but one which inherits a level of robustness and maturity of development that only comes after a number of years of use and modification The tool which
81. y EP6 we have that if t T then for every ep ep t B Dom The proof follows from the above lt Since 6Q 0 it follows trivially that Q meets condition DF It also follows that TQ r1 Q By this fact EP6 and the fact that Dom aB if bi bia we have that if t TQ then t out Q Domep It follows by EP6 and the definition of DP that Q meets condition DP Corollary 8 If Q meets conditions DP and DF then TQ TQ We define a separate specification process for each ep ep such that b bniq and carry out a refinement check in the traces model between that specification and Q with all events hidden which are not in aB We denote the specification process for each ep as DP and define it as DP DP where DP t Dac Next t a DP t o a The following result then lets us check conditions DF and DP using FDR2 14 J Burton Theorem 9 Q meets conditions DP and DF if and only if 5Q and for every ep ep such that bi bnia DP Er Q aQ aB Proof We first observe that TDP Dom by a straightforward induction on the traces of DP re spectively Dom The proof follows from the above theorem 7 and the fact that in the traces model w Bi w rQ 7 Q a aB 6 Checking condition TE The condition to be checked is as follows TE eztrepuep TDomQ STP When checking this condition we first assum

Compositional Verification of a Network of CSP Processes: using

Contents

Download Pdf Manuals

Related Search

Related Contents