Symbolic Semantics for CSP
Contents
1. SKIP n SKIP xix gt 0Ax lt 10 103 xx gt 0Ax lt 50 103 xx gt 50 103 Ax lt 100 103 c SKIP Kkx x gt 0Ax lt 100 SKIP m SKIP xx gt 0Ax lt 1000 xx gt 0 xix gt 50 D SKIP k xlx gt 0Ax lt 100 105 SKIP n SKIP x x gt 0Ax lt 10 10 xx gt 0Ax lt 50 106 x x gt 50 106 Ax lt 100 106 Figure 1 Example CSP CSPM semantics do not have rules for replicated operators Replicated Internal Choice Replicated External Choice etc Instead they view replicated operators as macros of their binary versions over sets This fact means that the original CSP and CSPM syntax cannot express a replicated operator if the set of the replicated operator is infinite such as the second and third Replicated Internal Choice operators in process C Even if the set is finite the cost is very expensive for CSP semantics based tools to run a small replicated process in a large macro such as the process D On the other hand HCSP semantics based tools can overcome this problem and run CSP processes regardless of the size of sets in replicated operators By using HCSP semantics the four processes in the example will have the same number of possible next moves In addition HCSP semantics based tools can expand the set of possible CSP processes to execute processes C and D above are examples of this fact We will see that this fact is useful in some real applications such as the medical mediator system in Gunter et al B This pap2. Y P p p HY 4_ P gt O Por xB x BAx4U Uda 1A t u Ua BU x y P U x gt y P 3p p HY ay P gt a Y P x B Rep_ext_tau Rep_ext_nor Figure 6 HCSP semantics category 3rd this semantics is an execution pattern corresponding to a possibly large or even infinite set of individual execution traces in the original CSP semantics For instance the HCSP semantics allows a potentially infinite collection of data in the set of replicated choice operators to execute as one single transition which is a nice feature that traditional CSP based analysis tools cannot provide The labels of the HCSP semantics will be ranged over by as follows I t UV The label represents process completion the label t represents a process performing an invisible action and the label U V represents a pair of a channel and a real action In any execution of a process in accordance with this semantics the sequence of transitions is labeled with mutually distinct pairs of parameters U V when not labeled by or t The values potentially represented by labels of the form U V are progressively restricted by the conditions in each of the subsequent triples resulting from each transition in the execution In this way a single execution in the transition semantics of HCSP potentially represents a parameterized family of executions from the original CSP semantics When translating the original C
3. 10 A W Roscoe S D Brookes amp D J Walker 1986 An Operational Semantics for CSP Technical Re port Oxford University Computing Laboratory Available at http www cs ox ac uk people bill roscoe publications 26 ps 11 J B Scattergood 1998 The Semantics and Implementation of Machine Readable CSP D phil Oxford University Computing Laboratory
4. rules displays the main difference between the CSP and HCSP semantics In CSP the Parallel rules specify individual transitions that are allowed while in HCSP whole families of transitions are specified hence the Holistic in HCSP In the CSP semantics there is a certain ambiguity in dealing with ill formed expressions The boolean guard in the If then else operator is an example of this Therefore it needs special treatment when merging the boolean guard into the existing condition We introduce a condition that includes the Wf operator applied to the boolean guard b of the If then else process to resolve the ambiguity This means that the If then else process can transition if and only if the boolean guard is fully evaluated and is actually a boolean In a given environment the expression for the boolean guard might or might not be capable of evaluating to a boolean value and it is important to distinguish the case of non evaluation from either evaluating to true enabling transition to the then process or false enabling transition to the else process For example in the HCSP process if x lt 1 then P else Q the else branch should be taken when x gt 1 not simply when x lt 1 does not hold since the latter includes the case when x is a list or something other than a number We do not want to transition to Q in the case where x is for example a string However the semantics of the parallel operator of HCSP instead uses the satisfi
5. with a potentially bigger scope than the one locally presented by P and y The main contribution of the paper is to provide a basic framework to translate transition semantics into symbolic semantics by merging state information in Floyd Hoare logic 4 with the existing seman tics The basis of our approach is to associate a state environment whose structure is implemented as a predicate with an evaluation of the semantics When we are going to evaluate a statement in a program ming language instead of evaluating the statement directly we view each transition as a constraint which can be merged into the current environment After updating the environment we can reason about the evaluation by asking about the satisfiability of the environment predicate For example if we translate the traditional semantics of CSP by our framework then the new semantics tells the users the range of values for a particular next possible move in CSP when the environment predicate is satisfiable or a next move is impossible because the environment predicate associated with it is unsatisfiable A trace in Li Gunter and Mansky 7 Uda ee p pE U cAV a Ny Act_prefix a v ca P CY Y qu V Ua U cAV aNy P U ga V UsUa Ap pE U cABV x A 7 Ext_prefix a y c x B gt P QU V Ua U cABIV x Ay PIV x Uga 3p p H BIU x y a rf D gt u U amp B U x A y P U x Rep_int_choice Uga uj Ua BU x AYP U x
6. 7 2 Stephen D Brookes C A R Hoare amp A W Roscoe 1984 A Theory of Communicating Sequential Pro cesses J ACM 31 3 pp 560 599 Available at http doi acm org 10 1145 828 833 3 Elsa L Gunter Ayesha Yasmeen Carl A Gunter amp Anh Nguyen 2009 Specifying and Analyzing Workflows for Automated Identification and Data Capture In HICSS pp 1 11 Available at http dx doi org 10 1109 HICSS 2009 402 4 C A R Hoare 1969 An axiomatic basis for computer programming Commun ACM 12 10 pp 576 580 doi 10 1145 363235 363259 Available at http doi acm org 10 1145 363235 363259 5 C A R Hoare 1985 Communicating sequential processes Prentice Hall Inc Upper Saddle River NJ USA 6 Yoshinao Isobe amp Markus Roggenbach 2006 A Complete Axiomatic Semantics for the CSP Stable Failures Model In Christel Baier amp Holger Hermanns editors CONCUR 2006 Concurrency Theory Lecture Notes in Computer Science 4137 Springer Berlin Heidelberg pp 158 172 Available at http dx doi org 10 1007 11817949_11 10 1007 11817949_11 7 Formal Systems Europe Ltd 2003 Process Behaviour Explorer ProBE User Manual In ProBE User Manual 8 Formal Systems Europe Ltd 2010 Failures Divergence Refinement FDR2 User Manual In FDR2 User Manual 9 Lawrence C Paulson 1990 Isabelle The Next 700 Theorem Provers In P Odifreddi editor Logic and Computer Science Academic Press pp 361 386
7. CSP semantics benefits from being able to handle such large or unbounded sets uniformly as single actions thus avoiding state explosion problems In addition to the simulator the work in this paper was all developed in the interactive theorem prover Isabelle This means that we have the additional recourse of using interactive proof methods such as structural and rule Li Gunter and Mansky 13 induction when analyzing the traces of a system such as the medical mediator While FDR2 can only check the above safety property for the combination of two patients two nurses two devices and two medical mediators using induction with HCSP semantics in Isabelle we can prove the safety property of the same process for an arbitrary number of patients nurses devices and medical mediators CSP Prover is a theorem proving tool built on top of Isabelle 6 It provides a denotational semantics of CSP in Higher Order Logic CSP Prover uses functions in places of terms with bindings to avoid issues of O conversion and substitution This formulation means that CSP Prover can express terms that are not expressible in standard CSP syntax Despite its extra expressive capability CSP Prover can not directly handle proving the desired safety property for the medical mediator again due to its direct implementation of the original CSP semantics While carrying out proofs manually can take advantage of the theorem proving setting much of the automation fails to be
8. ER _ _ Seq step Seq_check a 7 P Q a y P Q a 7 P Q a Y Q a n a YP ay P y P Hid_tau oo a 7 P k x B a 7 P k x B ay P k x B a Y a a aS a Y P a y 0 he 7 Parcheckl EEE A E E EOE EEEE Par_check2 a y P k x B Q a 7 QKk x BHO a 7 P i k x B Q a Y Pl k x B IQ a Y a Y P a 7 0 a 7 0 Par_taul z 7 Par_tau2 a y P k x B Q a 7 P k x B Q a PI k x B Q a Y Pl k x B IQ Figure 4 HCSP semantics category 1st In order to describe the HCSP semantics there are some functions that need to be supplied for the evaluations of user defined types A function procEnv must be defined for interpreting a given process name p where the process name p in the Proc_name operator denoted by in the concrete syntax in 6 Symbolic Semantics for CSP atte a Ifthenelsel Pe F en 2 u Ifthenelse2 a 7 if b then P else Q a b A 7 P a 7 if b then P else Q a b Wf b A y Q ay P E a Y P Ap p K BIU KIV x AY see a acces CY a BU K V 2 AY P k x1B a 7 P ay P SPP R BUM AY m a ARN a BIU K V x 7 P k x B a y P a it P 3p PE CBA AY oa a 7 Pli k x ByO a BI K V x Y P Kk xIBYIO a 7 0 E a Y 0 3p p H OBU KV xA ae a1 Pik x1B 0 a B
9. Lemmas Li Gunter and Mansky 11 5 Simulator To put the theory of HCSP into practice we have implemented an HCSP simulator with a rich mutually recursive datatype for actions and propositions in Isabelle We also extract the Ocaml code from Isabelle directly The core of the simulator is included with the package for the soundness and completeness theo rems In the simulator we have limited the propositions to qualifier free first order logic with Presburger arithmetic in order to maintain decidability In doing so we render the single step transition relation computable as a function generating a finite set of possibilities We then represent all possible traces with a lazy stream data structure supporting back tracking This enables us to incrementally compute the requirements for a given trace which can be inspected at each step and can be back tracked when the requirements are proven to be unsatisfiable Using the HCSP semantics we can indefinitely delay the calculation of a specific trace using trace patterns and pre and post conditions until one trace pattern condition is selected At this point satisfiability analysis can be used to generate an instance trace if such is desired In the case of the medical mediator we were able to use the simulator semantically embedded in Isabelle to enumerate the possible trace patterns for the System and to verify that all traces satisfying each pattern condition so enumerated sati
10. SP semantics into HCSP semantics the main task is to merge infor mation about actions and channels into the environment condition y and use this condition when we are trying to evaluate a CSP process To do so we will divide the transition rules in CSP into three categories rules for basic operators having no side conditions other than t label constraints rules with side conditions needing to be translated into the HCSP framework and rules for operators that were treated as macros in CSP The rules without side conditions are those for SKIP STOP Internal Choice External Choice and Sequential Composition operators For these we just need to add the set of free parameters and envi ronment conditions to the processes involved propagating constraints from hypotheses to conclusions in the original CSP rules For example the External Choice operator has the following semantics in the 8 Symbolic Semantics for CSP original CSP 14T a y P a 7 P 5 becomes f Ext_choicel P QO P a y P Q a 7 P lt P gt P The second category contains the operators with set or boolean guard information namely Parallel Hiding and If then else The general idea for translating the rules of CSP into HCSP is to treat the set information and boolean guards as new restrictions on the environment and merge them into the conditions as post conditions of the transitions after we do the same steps to transl
11. Symbolic Semantics for CSP Liyi Li Elsa Gunter and William Mansky Department of Computer Science University of Illinois at Urbana Champaign liyili egunter mansky1 illinois edu Communicating Sequential Processes CSP is a well known formal language for describing concur rent systems Brookes Hoare and Roscoe 2 have given a transition semantics for CSP that underlies common approaches to model checking properties of CSP programs In this paper we present a gen eralized transition semantics of CSP which we call HCSP that merges the original transition system with ideas from Floyd Hoare Logic and symbolic computation This generalized semantics is shown to be sound and complete with respect to the original trace semantics Traces in our system are sym bolic representations of families of traces as given by the original semantics This more compact representation allows us to expand the original CSP systems to effectively model check some CSP programs which are difficult for other CSP systems to analyze In particular our system can han dle certain classes of non deterministic choices as a single transition while the original semantics would treat each choice separately possibly leading to large or unbounded case analyses All work described in this paper has been carried out in the theorem prover Isabelle This then provides us with a framework for automated and interactive analysis of CSP processes It also give us the ability to ex
12. U K V s AY PIKK x B YO ay P a 7 0 9 a0 Ip pH U U AV V ABU KNV x AY UW a 7 P C a y PI k x B Q Par_in a U U AV V ABU KV x AYP k x B IO Figure 5 HCSP semantics categories 2nd Figure 2 is user defined and can be arbitrarily complicated A family of substitution functions T a x is needed for the replacement of variables by acts in each of acts boolean expressions and process names Using these we define the substitution function for processes There also needs to be a family of user defined evaluation functions for acts and boolean expressions and a models function for checking whether a boolean expression is true under a given assignment function The semantics for HCSP is given in Figures 4 to 6 It is a merge of the original CSP semantics given by Roscoe et al with ideas from Floyd Hoare Logic and symbolic computation We present a labeled transition system for HCSP over triples of the form y P where P is an HCSP process yis a proposition in HCSP that is intended to state the current requirements for parameters in scope including those occurring free in P and amp is a set of parameters large enough to contain all parameters occurring free in P or y The proposition y plays the role of providing the pre and post condition for each transition We carry with us to allow for the choice of fresh parameter names guaranteed not to clash
13. and the broadcast system synchronizing on the music requests Finally the Center process models the whole karaoke center In the Center process we use a Replicated Interleaving operator to represent the behavior in all twenty five rooms It indicates that the twenty five rooms have no communication interactions The capital letter N refers to an arbitrary number to represent the size of the database that contains all songs in the song broadcasting system Typically we know that the number N is a large number but we do not know exactly how large it is In order to verify properties in the system such as safety and deadlock freedom it is better to leave the number N to be unspecified Obviously original CSP based tools such as FDR2 and ProBE cannot deal with the case when N is unspecified Even specified but very large values can not be handled For example when we test the case when N is 100 000 in ProBE the program fails to start On the other hand the HCSP semantics can handle the model with only a few transitions This fact indicates that the HCSP semantics can be useful in cases previously not handled and it will expand the category of CSP programs for which we can perform automated analysis 7 Related Work Currently there are several existing CSP simulators and model checkers based on the original CSP transition semantics CSPM gives a standard CSP syntax and semantics in machine readable form introduced by Bryan Scattergood which is b
14. anslating these rules into HCSP rules we follow the same procedure as for the rules in the second category except that we add new hypotheses to indicate that the parameters such as U and V in the Ext_prefix rule are not in the existing parameter set a 4 Correctness of HCSP with Respect to CSP In this section two main theorems are proved to show that the HCSP semantics is sound and complete with respect to the original CSP semantics Our reference semantics is the CSP transition semantics introduced by Roscoe Brookes and Walker 10 with the updated syntax of CSP Prover 6 All of the work described here has been formally carried out in the interactive theorem prover Isabelle HOL Our Isabelle code may be found atttp aww cs illinois edu egunter fns HCSP hcsp The proofs of soundness and completeness of the HCSP semantics are parameterized by user defined acts which correspond to user defined values in the original CSP semantics These proofs are also parameterized by a user defined set of process names together with their associated processes given by procEnv and a notion of freeParams satisfying freeParams procEnv p C freeParams p for every process name p In the Isabelle code for HCSP the values and acts are two different types but in this paper by common abuse of notation we will assume that values and acts have the same type We use m and n to refer to values below In the Isabelle code we must also have a separate f
15. applicable to code such as was given in the medical mediator example CSPsim 1 is another simulator based on the FDR2 standard Its major innovation is the use of lazy evaluation The basic idea of CSPsim is to keep track of all the current actions then compare them with the actions of the outside world and only select the possible executable actions for the very next step I The phrase lazy evaluation refers to a pre processing step in which CSPsim selects some processes that contain fewer actions and generates some conditions in advance After that CSPsim evaluates the whole program based on these conditions For instance if a program has a STOP process in a branch of the parallel operator the next possible action can only be a T action Hence the CSPsim will select the STOP process as the very next step resulting in fast feedback Nonetheless after generating all the possible states for the next step it still must compare possible actions with those provided by the outside world one at a time instead of considering a group of properties 8 Conclusion and Future Work In this paper we have presented HCSP a new semantics for CSP HSCP provides an alternative way to model CSP processes by viewing transitions as bundles of the original transitions where all transitions in the bundle can be described by a uniform property derived from the process By this translation we can allow HCSP based tools to run some CSP programs which are
16. ased on the transition semantics introduced by Brookes and Roscoe 10 It provides a standard for many CSP tools including FDR2 the industry standard for CSP model checkers 8 FDR2 uses the traditional view of actions as single elements and so tends to generate a large number of states when comparing multiple possibilities for actions ProBE isa simulator created by the same group which simulates a CSP process by listing all the actions and states one by one as a tree structure 7 Additionally traditional CSPM semantics based tools such as ProBE and FDR2 treat some operators especially replicated operators as macros and hence it is impossible for these tools to generate traces when the replicated set is infinite The medical mediator project by Gunter et al provides a example of the advantages of HCSP over CSP semantics based tools The main goal of the medical mediator project is to prove that the set of traces of the process System Vis Given is a subset of the traces of Safety Vis Given where Vis is a set defined as y 3n d m x y RFIDChan x V Am z y EHRBECh z See Fig B This requires exploring all possible traces generated by the System process Tools based on the original CSP semantics such as FDR2 fail when dealing with large or unbounded sets For example the Med process as given does not put any restrictions on the sets of values that may be received over various channels The simulator we have built based on H
17. ate the rules as were done with the first category This requires us to translate all set information into set comprehension notation For example for the Parallel operator we make the following translation rex PLP 05g becomes PiX gt P x Q 3p p H U U V V AB U k V x A y rp 9 yP yo E yo a 7 PIi k x By Q T a U U AV V A BIU KIV x A7 PKK x1BYIQ This rule means that a Parallel process can communicate between the left hand side and right hand side sub processes if they can produce the same action and the action is a valid action in the middle set of the Parallel process the Parin rule Other rules allow each sub process to progress independently For rules in this category we replace labels by parameter pairs U V giving a fresh parameter pair for each transition hypothesis This allows for separation of the constraints for each of the hypotheses In the Par_in rule since we need to make sure that the actions produced by the left hand side and right hand side sub processes are equal we also need to put into the final environment condition the condition that the two actions are equal Also we must add a requirement that the label in its two parts U and V satisfies the set constraint of the Parallel operator After we finish constructing the new condition we need to verify it and see whether or not there is an assignment function p that models the new condition The translation of the Parallel
18. ent y be an environ ment condition such that p y and a be a parameter set such that freeParams P UfreeParams y C a Further suppose we have a CSP process T and a value i such that sem p P T in CSP semantics Then there exist an HCSP process P an assignment p an environment condition y a parameter set a and a label l such that i sem p 1 P la Pla T sem p P p Y and a 7 P a y P Proof Sketch By induction on the CSP semantics rules For each rule in HCSP the first thing we need to do is to use Theorem 4 1 and Lemmaf4 4 to prove the theorem hypotheses for the inductive instances Then we will interpret P a y and p according to the corresponding HCSP rules and show that the interpretation is correct For each rule since the only parameters generated from the evaluation of an HCSP process are parameters not in set we can always make a new assignment function p based on the current p and p y_ P q To show that i sem p we need to do a case analysis on all possible labels an HCSP process can produce given the fact that there is always an interpretation for a given free parameter U Finally in some rules we need to show that the p we are selecting can properly model the post condition of the environment To prove this we must use the same technique as we use in reasoning about the post condition in the Soundness theorem and a uniform group of lemmas represented by
19. er s contribution is a new formalization of CSP syntax in Section 2 and semantics in Sec tion3p which we have proved correct proof sketched in Section 4 and supports simulation Section 5 Along with the semantics in Section B we will also talk about how to transfer a rule in original CSP into HCSP by adding additional information to the transitions Before that we demonstrate the expres siveness and power of HCSP as compared to traditional CSP semantics by using examples Finally we reason about where the power comes from in Section 7 and provide one more example in Section 6 to show that there is a large collection of problems which are hard to be analyzed in CSP framework can be reasoned in HCSP framework All of the work described in this paper has been formalized and proved in the interactive theorem prover Isabelle HOL 9 2 Syntax The syntax of HCSP is given in Figure For the remainder of this paper the following name conventions will be used We will use P and Q for processes Lower case p refers to an HCSP process name The Li Gunter and Mansky 3 P Q Successful termination SKIP Awaiting successful termination STOP Unexpected termination c a gt P Prefix by action a on channel c if b then P else Q If statement p Process name p as prcoess P Q Sequential execution POQ Binary external choice PNQ Binary internal choice P Replicated internal choice xB c x BP External set prefix P Replicated e
20. es versus fails to satisfy meaning of boolean expressions For instance in the process P k x k c Ax lt 1 Q if the process P commits a string action of c hi the whole process can actually make a further step by a single non communicating move in P by the original CSP transition semantics Par_in Li Gunter and Mansky 9 The third category includes all replicated operators which in CSP are considered to be macros based on other rules The ones we have included are the Replicated External Choice Replicated Internal Choice and External Set Prefix operators For example the Replicated Internal Choice operator has the following macro definition in CSP P Pla x NP a2 x N where a1 a2 S We will translate xi the rules of these operators from CSP into HCSP by their semantic meanings This means that we will create new rules that are semantically equivalent to the macros for these operators For example we create new rules for Replicated External Choice for the original CSP as follows acs Pla x gt P IAT aes Pla x gt P TT Rep ext_tau x S P Ox S a P OP Rep_ext_nor x S P 5 P Relying upon the associativity and commutativity of Replicated External Choice in the original CSP these rules can be seen as special instances of the rules for the corresponding binary operators Having added these rules to CSP when tr
21. he scope of the xB xB variables k and x is only the proposition B in the processes P k x B Q and P k x B The syntax of HCSP differs from that of CSPM by Bryan Scattergood in three ways Firstly the actions of CSP are explicitly divided into channels and actions written c a in HCSP syntax Secondly for the sets used in constructs such as the parallel composition of two processes or replicated internal choice we use a set comprehension notation This decomposition of sets into variables and predicates will facilitate the statement of the transition rules of HCSP semantics Finally HCSP currently lacks the CSP Renaming operator HCSP is parameterized by four user defined types a type of expressions for actions and channels acts a type of propositions a type of process names and a type of values to be assigned to acts and boolean expressions The language of boolean expressions must minimally support conjunction nega tion equality and a special operator Wf ranging over boolean expressions while the language of acts must minimally support a function injecting the disjoint sum of variables and parameters into acts The Wf operator checks whether a given proposition is well formed in a given environment in the sense that it can be evaluated to a boolean value in that environment In the semantics section we will see how Wf is useful in distinguishing between the different interpretations of boolean expressions in the If then else opera
22. hile the Med and the unlisted MedRead processes model the identification system The unlisted EHRInterface process models the backend system for delivering information displayed on the mediator and collecting data transmitted from the mediator The unlisted TakeCKReading process is used in the Nurse process to model the behavior by which a nurse verifies a reading from a patient B The BTDevs process models the behavior of announcing Bluetooth channels to the mediators scanning for them It is part of the unlisted process Given Finally the System process combines the Nurse process the Med process and the EHRInterface process together using the Parallel operator and limits the set of actions that these three processes can communicate to the set in the middle of the Parallel operator The Replicated Interleaving operator P in the System process uses the CSP macro P P m x m xm P m2 x where m m2 x m It means that all its sub processes do work individually and do not communicate at all We keep the same macro in HCSP semantics because it would allow the infinite parallel processes occurred in a program if we allowed infinite set in the Replicated Interleaving operator which is a fundamental change for the meaning of the CSP language In the original CSP definition the External Set Prefix operator c x B P is defined as a macro as Je P In HCSP we provide the operator with a semantic interpre
23. mplex boolean expressions However we believe this methodology could lend useful insights to the transition semantics of other systems as well 14 Symbolic Semantics for CSP For further study we are interested in combining the ability to reason locally about code fragments by induction with an automatic model checker The model checker should be directly related to the HCSP semantics in Isabelle In this way we can prove the correctness of our HCSP model checker with respect to the HCSP semantics The new model checker will be able to check some programs that are hard to analyze with traditional CSP tools In another direction we will try to build a dependent session type system for the HCSP framework We believe there may be interesting synergies between dependent session types and symbolic execution traces 9 Acknowledgments This material is based upon work supported in part by NASA Contract NNAIODE79C and NSF Grant 0917218 Any opinions findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of NASA or NSF References 1 Phillip J Brooke amp Richard F Paige 2007 Lazy Exploration and Checking of CSP Models with CSPsim In Alistair A McEwan Steve A Schneider Wilson Ifill amp Peter H Welch editors CPA Concurrent Sys tems Engineering Series 65 IOS Press pp 33 49 Available at http dblp uni trier de db conf wotug cpa2007 html BrookeP0
24. nal from one of the clickers will honored immediately while the other signal will be delayed for later action We model the karaoke center in CSP in the Figure 7 We will use the Clicker process to model the behavior of a remote clicker in a karaoke room The input argument c is the clicker s identity and r represents the room to which the clicker belongs The Clicker allows the user to select any song in the database represented by the second Replicated Internal Choice operator over s s gt OAs lt N where N is the size of the song database 12 Symbolic Semantics for CSP After the song has been decided the Clicker process sends out the message K r c s by the Action Prefix operator where K is a channel representing the karaoke center The whole sequence K r c s means that in room r of the karaoke center clicker c was used to select the song s We will use the Broadcast process to represent the behavior of the song broadcasting system in a room It will wait for the signal from one of the clickers telling which song to play These choices are represented by the two Replicated External Choice operators Having received the song request it will broadcast the song in the room originating the request This is represented by Action Prefix operator with the sequence K r s The Room process with id r represents the behavior of the room as a whole The room is a parallel composition of the two clickers in the room with no communication between them
25. not able to run in the original CSP based tools We have shown the HCSP semantics to be equivalent to the original CSP transition semantics We have also presented an HCSP based simulator which is extracted directly from the Isabelle code for the HCSP semantics and shown that it is not only theoretically powerful but also practical to implement By using the medical mediator project as an example we show that the HCSP semantics implemented with Isabelle s system for inductive rule definition and reasoning can overcome some difficulties that traditional CSP semantics based tools cannot handle The ideas represented in this alternate semantics are applicable beyond the example of an alternate semantics for CSP Roughly the methodology applied here may be described as a two phase transfor mation In the first phase we transform a substitution based transition relation into a corresponding environment based transition relation In the second phase we transform individual transitions into symbolic transition patterns replacing environments by predicates over system variables giving pre and post conditions for our transitions These conditions are derived from the tests present in the processes being transitioned and the side conditions of the original transition rules This methodology has a par ticularly significant pay off for CSP where the behavior of many operators such as the replicated choice operators are predicated on the satisfaction of co
26. ns In HCSP we can view a set of actions as a whole in some contexts but also divide it based on various properties in other contexts The differences between the original CSP semantics and the HCSP semantics are large enough to be visible in some very simple examples Four such examples are shown in Figure I We tested these examples by using FDR2 to determine whether the processes refine themselves FDR2 takes several seconds to run process A and several minutes to finish the proof for process B It fails to terminate on Submitted to Li Gunter and Mansky 2 Symbolic Semantics for CSP processes C and D On process C it begins to run but eventually faces a stack overflow it claims that process D exceeds the integer limit for FDR2 even though the FDR2 User Manual suggests that 32 bit integers can be handled 8 Also when we directly input process C into the CSPM based simulator ProBE the whole program crashed without leaving any information However the HCSP simulator we have derived from the semantics given in this paper takes two or three seconds to list all the traces for all four processes From these examples we can clearly see that the running time of FDR2 depends on the size of the set in each process These facts reflect in part that the original CSP and Machine Readable A SKIP k xlx gt OAx lt 100 SKIP n f SKIP xx gt 0Ax lt 10 xix gt 0Ax lt 50 xix gt S0Ax lt 100 B SKIP kxx gt 0 x lt 100x10
27. r in the System process because the set of the Parallel operator includes all communication along all the HCI channel The Parallel op erator Nurse n mm HCI x True Med n m allows interleaving actions to happen if the actions from Nurse n m and Med n m do not belong to the middle set while it allows communication between processes Nurse n m and Med n m through the same action if the action belongs to the middle set Finally the Hiding operator is used to make a transition become local i e invisible to the outside world it provides security for the process involved For example the System process hides a transition if the transition s belongs to either of the HCI or EHRCh channels This means that the System process does not want outside processes to see and affect the actions along the HCI and EHRCh channels 3 Semantics a y Qk xB 4 a Y Q Par omega y SKIP gt a 7 Q Skip a 7 p gt amp y procEnv p Proc_name T y PNQ gt a 7 P Int_choicel a 7 PNQ 5 y Q Int choice2 at y P gt a P l a 7 0 gt a 7 0 l Ta 7 Ext_choice_taul 7 7 Ext_choice_tau2 a 7 P0Q a ie 0 a y POQ gt a 7 POQ 14t amp y P gt a 7 P L t a 7 0 gt 0 70 Ext_choicel j 7 7 Ext_choice2 a 7 P ER rar a POQ a 7 0 14y 0 P 5 a 7 P arP
28. r set a such that freeParams P UfreeParams Y C a if a y P a 7 P then sem p P sem p P Proof Sketch By induction on the HCSP semantics rules It is worth noting that each assignment function p is a total function and thus gives some value to every parameter regardless of whether the parameter has been included in the parameter set Each rule in HCSP has a corresponding rule in CSP When we prove soundness we must show that for each rule in HCSP if the hypotheses of the rule are valid in HCSP then the corresponding hypotheses of the corresponding CSP rule are also valid This follows from Theorem and the fact that the environment condition y only becomes logically stronger with each transition Handling the rules for the replicated operators requires use of Lemmaf 4 2 The hypotheses in the CSP rules include side conditions that have become incorporated in the environment condition in the derived HCSP rule It is therefore necessary to prove these side conditions from the assumption of the validity of the initial environment condition and the specifics of the transition in HCSP For this we need to make use of Lemmaf4 3 As yet HCPS does not support all processes in CSP In particular there is no support for the Re naming operator As a result our completeness theorem is restricted to that portion of CSP supported by HCSP Theorem 4 6 Relative Completeness Let P be an HCSP process p be an assignm
29. sfy a pattern condition of the Saftey process 6 One More Example Clicker c r K r c s Clicker c r Broadcast r K r c s s gt O0As lt N gt K rs Broadcast r ss gt 0A c true S lt N Room r Clicker c1 r Clicker c2 r k x dc s k K r c x s Broadcast r Center Room r rr gt 0A r lt 25 Figure 7 Example Besides the small example in Fig and the medical mediator example from Gunter et al B there are many other real implementations that can benefit from modeling in the HCSP system Generally speaking every real model with several users trying to access one or more copies of a very large database can benefit from the HCSP system A song broadcasting system is one such example Song broadcasting systems are used in entertainment businesses such as discos and karaokes to allow people to select songs from a large database Such systems typically have a large collection of songs a collection in excess of 100 000 would not be uncommon A typical karaoke bar has about 25 rooms for separate entertainment Typically each room has two remote clickers for selecting the next song to be played After a user selects a song the remote clicker will send the song selection to the song broadcasting system and the song broadcasting system will play the chosen song in the room Since only one song will be broadcast at a time if two people send their selected songs through clickers at the same time only the sig
30. tation because the operator is uset in representing receiving in CSP and it generates fewer vacuous rule applications than the specialized instance of the Replicated External Choice operator Also the c a P operator that appears in the Nurse process of the medical mediator project is the same as c a P as according to the CSP book 5 In the CSP world there is no notion of sending and receiving messages instead they use the notion of internal choice and external choice to represent sending and receiving For example in the Nurse process the operator HCI RFIDChan P means that we internally commit an action RFIDChan on the channel HCl where both action and channel are previously internally selected select a value GetID for the HCI channel On the other hand in the Med process the operator HCI 2x P means m Li Gunter and Mansky 5 that we externally wait to receive every possible value through the HCI channel The the operator HCI x P uses an abbreviation of x as x True where we omit the set predicate True here In addition in the System process we select a mediator from the Replicated Interleaving operator and a nurse from the Replicated Internal Choice then select the corresponding channel from the HCI chan nels this channel will be used in the Nurse and Med processes as the HCI channel Then these two processes Nurse and Med can communicate via the Parallel operato
31. tor versus in the Parallel operator in HCSP In some cases the advantages of HCSP will cause significant differences when we are trying to 4 Symbolic Semantics for CSP Nurse n m System AUTI Nurseta n etn aver HCI GetID gt m HCI RFIDChan p Med n m EHRChm x True HCH RFIDChan HCI 2x EHRInterface y Vn m p d x d y RFIDChan x A y 4 EHRBECh x A ifx G Ai Name d y BTAddrs x Ay amp BTScanm x then HCI Yes TakeCkReading n m p d else if x Error then HCI OK Skip else HCI INo Skip m System Med n m HCI GetID gt HCI 2x1 gt 21291 gt HCI 2x2 x2 v2 gt EHRCh 1 v2 EHRCh 271 if m Error then HCI In HCI 20K gt Skip BTDevs Of tt BTScanm X gt BTDevs else EHRCh 2nz HCI n1 n2 gt HCI2z gt E if z Yes then MedRead n m elseSkip Figure 3 Part of Medical Mediator Project Code analyze traces through CSP tools One such example is the medical mediator project B The medical mediator project provides a formal model of the use of a device for Automated Identification and Data Capture AIDC for vital signs measurements in hospitals 3 To demonstrate our HCSP semantics we provide a small piece of the CSP code for the medical mediator project in Figure 3 and describe here the operators occurred in the code The Nurse process models all behaviors that nurses can do with the mediator w
32. tract Ocaml code for an HCSP based simulator directly from Isabelle 1 Motivation Communicating Sequential Processes CSP is a kind of process algebra for modeling concurrency When using CSP to model a complex system such as the medical mediator system in Gunter et al 3 a common problem is that one piece of a CSP process can generate a large number of similar ac tions For example the CSP process c x B P is generally modeled as receiving a single value from the set x B If B describes a nonempty set the execution of the process will depend on the size of the set in traditional CSP tools In practice if the set x B is an infinite set many CSP simulators will actually create an endless number of similar processes and wait for other parts of the program to stop these processes In this paper we present Holistic CSP HCSP a new semantics for CSP processes that uses a symbolic representation of actions to capture a group of properties simultaneously instead of considering only a single element with a single property The approach we take in this work is to represent families of transitions in CSP by a single transition in HCSP In some implementations of CSP simulators such as the JCSP package in Java actions are im plemented as objects allowing sets and other complex objects to be passed as actions through channels However this is still a single action instead of a property describing a group of actions and corresponding transitio
33. unction for each type of construct we need to translate from HCSP to CSP By and large these functions are just the obvious translations Here we will abuse notation and uniformly refer to them all as sem Before stating the soundness and completeness theorems a very important observation is that transi tions properly track the parameters introduced Theorem 4 1 Well tracked Parameters Assume we have a transition 7 P ay a y P in HSCP such that freeParams P U freeParams 7y C a Then freeParams P UfreeParams y C a Proof Sketch By induction on the HCSP semantics rules since the resultant a always contains both a and any new parameters The replicated operators use that freeParams P C a implies freeParams P U x C au U 10 Symbolic Semantics for CSP The proofs of soundness and completeness require the following facts describing how parameters assignments substitution and translation interact Lemma 4 2 Ifp U n then sem p P U x sem p P n x Lemma 4 3 fp B U x V y and sem p U and sem p V are well defined then p U p V is in the set sem p x y B Lemma 4 4 ffreeParams P C a p a P q then sem p P sem p P With these we can show that every interpretation of every transition we can take in HCSP is valid in CSP Theorem 4 5 Soundness For all HCSP processes P P assignments p environment conditions Y y such that p y and p Y and paramete
34. xternal choice xB P k x B Q Parallel composition P k x B Hiding over a set of actions Figure 2 HCSP Syntax c represents an HCSP channel while the a represents an HCSP action In HCSP in Isabelle a channel and an action have the same user defined type which we will refer to here as the act type The B is a proposition describing the property of a set In HCSP we include both variables and parameters which are distinct types We use k for variables ranging over HCSP channels and x for variables over actions We use U and V to refer to parameters ranging over channels and actions Variables and parameters serve similar functions but differ as follows variables may occur free or bound in HCSP processes and may be replaced by actions or channels by substitution while parameters occur essentially as local constants not subject to binding or substitution In the rest of the paper we will use freeParams to refer to a function returning all free parameters in an expression of arbitrary type Transitions will be labeled by T see Section 3 or pairs of parameters one for a channel and one for an action We will use l to represent a transition label Finally the Greek letter p refers to an assignment function that assigns values to parameters One remark that must be made here concerns the scope of variables In the processes c x B gt P P and _ P the scope of variable x is both the proposition B and the process P while t
Download Pdf Manuals
Related Search