CSP + Clocks: a Process Algebra for Timed Automata
Contents
1. 1989 Jo l Ouaknine Discrete Analysis of Continuous Behaviour in Real Time Concurrent Systems PhD thesis 2001 Jo l Ouaknine and J B Worrel Timed CSP Closed Timed Automata In Proceedings of EXPRESS 02 2002 A W Roscoe Model checking CSP In A Classical Mind Essays in Honour of C A R Hoare Prentice Hall 1994 A W Roscoe Theory and Practice of Concurrency Prentice Hall 1998 G M Reed and A W Roscoe A timed model for communicating sequential processes In Proceedings of ICALP 86 pages 314 323 Springer LNCS 1986 Steve Schneider Timewise refinement for communicating processes Science of Computer Programming 28 1 43 90 1997 S Schneider Concurrent and Real time Systems The CSP Approach John Wiley and Sons 1999 Sergio Yovine Model checking timed automata In European Educational Forum School on Embedded Systems pages 114 152 1996 Sergio Yovine Kronos A verification tool for real time systems kronos user s manual release 2 2 1997 W Yi P Pettersson and M Daniels Automatic verification of real time communicating systems by constraint solving In Proc of the 7th Interna tional Conference on Formal Description Techniques 19942. execute a b for the successive n time units This is a safety property that can be specified as a trace property The most non deterministic process that respects this property is S a tt gt jx Si Ele tt 5 S a tt gt la St Coget lt n 51 Eh lee gt n gt 5 This is the specification process against which processes are checked To en able refinement another process is needed in order to check whether a processes P refines the specification S we need to reset the clock x each time an action a is performed We can do this by defining a processes T a tt gt xh T where zx is a clock used only by T i e it is an external clock for P that performs this function The refinement that we need to check is the following S Err P T a where the refinement is with respect to clock x only This works because the specification S does not allow the execution of any b before the value of clock x is greater than n and the passage of time is recorded by delay actions Clock hiding is defined as a combination of hiding and renaming on the set of traces and the operational model if we hide a clock x then we need to hide all the reset or delay actions that involve it or rename the action if other clocks are reset or change region at the same time This is why we add the information of which clocks cause a region change to delay actions instead of having a single generic del
3. CSP Clocks a Process Algebra for Timed Automata Stefano Cattani and Marta Kwiatkowska School of Computer Science The University of Birmingham Birmingham B15 2TT United Kingdom stc mzk cs bham ac uk Abstract We propose a real time extension to the process algebra CSP Inspired by timed automata a very successful formalism for the specifica tion and verification of real time systems we handle real time by means of clocks i e real valued variables that increase at the same rate as time This differs from the conventional approach based on timed transitions We give a discrete trace and failures semantics to our language and de fine the resulting refinement relations One of the main advantages of our proposal is that it is possible to automatically verify relations be tween processes we will show how this can be done and under which conditions 1 Introduction The specification and verification of concurrent systems has been one a major research topic for more than twenty years Many approaches have been proposed and that of process algebras e g CSP Hoa85 and CCS Mil89 is undoubtedly one of the most successful Our work will focus on CSP by extending it with real time constructs The key features of classical CSP are a denotational model based on traces and failures together with the definition of process equivalence founded on the concept of process refinement Refinement which is defined as reverse inclusion of behavio
4. Jackson s thesis Jac92 shows how to translate Timed CSP processes into timed automata in order to use timed automata techniques to verify logical properties of processes More recently equivalence between Timed CSP and closed timed automata has been proved OW02 and it has also been shown how to extend digitisation techniques to timed automata in order to use FDR2 to verify refinement of timed traces We are aware of some work done to formulate process algebras that model timed automata directly D A99 YPD94 but to our knowledge no attempt has been made to use extend CSP to model timed automata directly this is the approach that we take in this paper We employ the successful techniques of timed automata e g the region automaton to discretise the infinite state space caused by the representation of time in order to define a semantic model and refinement relations in style of CSP Firstly we extend the syntax to describe timed automata s specific constructs The operational semantics is a straightfor ward extension of the usual CSP rules but defining a denotational semantics is more problematic the reason for this is that we have to deal with undecidability results because of the continuous representation of time and with obstacles in defining the semantics in a compositional way We describe how we resolve these difficulties and the inevitable resulting trade offs The main result is that it is possible with some limitations
5. PnQ 4P FIP FPN pS Pp PES Pp P A PAA A P AES Paa tea PSP PY P Q23 QR E52 pI HEA a P1AP2 py 7 P Q gt P free Q P Q P Q Pia Pp P42 P Q S PQ PQ amp Q T a gt P tt Ilo gt P p I P L X P Z P L free P T P T PNQ Z P AT Q T POQ Z P VZ Q T P Q Z P AT Q L up P ff T P A I P _T F P P T P Q P K a p P 0 K y P a K X P X U K P K free P K PNQ 0 K POQ K T K Q K P Q P U K Q k up P 0 K P A K P _K f P K P _K P Q K P Table 2 Operational Semantics in terms of Timed Automata actions are the same and Z and are defined according to the rules of Table 2 note that for the binary operators O M and also the symmetric rules hold We have introduced the silent action 7 which is the result of some internal computation usually caused by internal choice or hiding We have an extra special label v with no guard to denote successful termination and an extra process 2 that denotes the process that has successfully terminated In the following we will use the region automaton obtained from the opera tional semantics as the model we have in mind to define the denotational models for CCSP Given a CCSP term P and the associated timed automaton A P we denote the region automaton corresponding to A P with initial region r by R P r If we want to add an extra invariant to the initial location i e T P T P Av we d
6. ay action that would not allow hiding of clocks The trace model is enough to specify safety properties as what is needed is to include all those traces that do not present undesired behaviour If we want to verify liveness properties then we need to use the failures model The idea is the same as described above that is verify refinement with respect to only some clocks It would be possible to verify properties like strong bounded response by defining additional processes as above Finally it is possible to have successive refinements considering the example above if the following two refinements hold S Err Pi T Err PR T a a then both P and P respect the bounded invariance property and in addition there is functional refinement between P and Py Examples on FDR2 We have not tried the above examples on FDR2 be cause of the complexity of manually translating processes into equivalent CSP processes We tested our ideas with small toy examples in the following way firstly we defined small Clocked CSP processes then we translated them into the equiva lent timed automata and from here into the resulting region automata At this point we manually specified CSP processes equivalent to the region automata and verified refinements between them with FDR2 Given the complexity of building a region automaton it would be desirable to make the process above automatic Considerations With the approach we have propose
7. bing the change of region the elements of A are dx where X 2 We can now define the region automaton corresponding to a timed automaton A Definition 2 Given a timed automaton A the corresponding region automa ton Ry Qr Xr qr gt r is defined as follows Qr l r LE LU free L r Ry D XUAU with A x X CC dr l ro C Qr x Xr X Qr such that e Lr lr a X if for allv Eer l v Sus V v lr gt lr X X CC if for alver r Sis 1 v X 2e l succ r if for allv r there exists d such that L v EA l v with v succ r and X clocks r Region automata are the basis for any algorithm to model check timed au tomata and they are an important technique to discretise the infinite state space of the induced transition system Complexity is their main drawback as the number of regions is exponential in the number of clocks and constants For this reason more efficient techniques have been devised e g zones see Yov96 for an introduction CSP CSP is a process algebra introduced by Tony Hoare Hoa85 It describes concurrent systems in terms of their sequential components characterised by the sequences of actions that they can perform CSP processes with action alphabet X are generated by the following syntax P STOP SKIP a gt P PNP POP IEE eel eee 5 where a X AC X and f X X is a renaming function The operators above represe
8. by con sidering an untimed CSP specification and a Timed CSP implementation It is possible to verify whether the functional behaviour of the implementation refines the specification This approach is clearly limited because no timed properties can be verified moreover it is not possible to have chains of refinements More interesting and promising is the work on digitisation this technique has been known for at least 10 years in the area of timed systems and its main purpose is to identify the conditions under which it is possible to reduce the dense represen tation of time to a discrete one while preserving the relations among processes Oua01 has extended such techniques to Timed CSP making it possible to use FDR2 to verify refinement relations The main problem with this technique is that it is in general undecidable to know whether digitisation techniques can be applied In the domain of real time systems the most successful approach is arguably that of timed automata AD91 Timed automata extend traditional labelled transition systems with clocks real valued variables that record the passage of time and influence how the system evolves The success of timed automata is due to the availability of model checking techniques that allow us to verify properties expressed in the logic TCTL ACD93 and efficient model checking tools are available e g Uppaal LP Y97 and KRONOS Yov97 Some work has been done to relate CSP to timed automata
9. d we are able to verify refinement between processes and also both safety and liveness properties More importantly timing aspects of processes are considered possibly only those that we are interested in Unfortunately our approach has some disadvantages One and possibly the biggest disadvantage is complexity the number of regions corresponding to a timed automaton is exponential in the number of clocks and size of constants this is carried over to our setting making model checking possible only for small systems or systems with few clocks Another smaller drawback is the fact that we have to manually specify process specifications as we did for the example above It would be interesting to find a way to automatically generate such processes from some an appropriate logic 6 Conclusions In this paper we have described a proposal for a timed extension to CSP called Clocked CSP We have defined its semantics and the corresponding refinement relations showing how it would be possible to use the model checker FDR2 to verify such relations and also some timed properties of systems Possible future work will be aimed at improving the complexity of model checking investigating whether it possible to use known efficient techniques for timed automata in our case it would also be interesting to define a logic that could be verified with our technique Finally we plan to compare our approach with other similar approaches to extending CSP with
10. enote the resulting region automaton by R P r y We use R P as an abbreviation for R P ro tt 3 2 A Denotational Semantics for Clocked CSP By working on the operational model defined above one could use known equiv alence relations for timed automata e g timed bisimulation or use traditional model checking techniques to verify whether a given process meets some tempo ral logic property Following the CSP tradition we wanted to give a denotational semantics to the language that would extend the usual trace failures semantics and lead to refinement relations While deciding what kind of denotational semantics to give to the language we had to make several choices We had in mind two main issues Decidability We want the refinement relations generated by the semantic model to be decidable Our aim is to be able to use or extend FDR2 to automatically verify refinement for our processes This excludes the use of timed traces that is the traces obtained in the labelled transition system associated with a timed automaton it is known that timed trace inclusion and equivalence are undecidable for timed automata AD91 Compositionality We want to be able to define the semantics of a process in a compositional way that is to define the semantics of a composite process in terms of its smaller components This turned out to be not an easy task clocks can be seen as shared variables so when two processes execute con currently as the re
11. it under some conditions on clocks we therefore do not want a process to alter these conditions in a hidden way Table 3 reflects these new conditions on external choice by showing the modified SOS rules for this operator Finally we require the structure of a term to reflect the corresponding timed automaton by having all clock resets and the invariants preceding the other op erators i e those enabling transitions This can be achieved through syntactic transformations that preserve the operational semantics 4 1 The Semantic Model We give Clocked CSP processes a semantics in terms of region traces A region trace is and element of RTraces 7 UAU2 where X is the process alphabet A is the set of delay actions and C is the set of clocks So an element of a trace either denotes an action the passage of time delay action or the reset of some set of clocks We need to be able to define the semantics of a process from any possible starting region and under any possible initial invariant Consider for example the process a x lt 1 P its semantics depends on the semantics of the process P starting from 3 possible regions x 0 0 lt xz lt 1 and z 1 For this reason the semantics of a process is the set of possible behaviours under any possible starting condition The refinement relation is extended ac cordingly as reverse set inclusion under every starting condition Formally let R ri 1r2 1n be the set
12. k constraints by y We omit the interface alphabet of parallel composition when implicit or not relevant Most CSP constructs are kept unchanged a few have been modified in order to handle clocks we have guarded actions an action can be performed only when the condition on the clocks is satisfied we have a reset operation X that performs the resetting of the set of clocks X to 0 we have an invariant operation amp corresponding to the idea of invariant of timed automata 3 1 Operational Semantics Since Clocked CSP is designed to model timed automata the operational se mantics is intuitive and it extends CSP semantics in the obvious way For the purpose of giving semantics to Clocked CSP we introduce an extra operator free P representing a process that behaves exactly like P but which does not perform any initial reset i e the start state has been stripped of its resets We denote the set of all CCSP processes by CCSP and the set of all CCSP processes with the free e operator by CCSP Given a CCSP term P we define the corresponding timed automaton A P L l X U 7 C Z where L CCSP I P the sets of clocks and SKIP 2 up P Z5 Plup P p PE a p P mie gt P 2AP pep P P p P Pp X P P free P 25 P P 4P T P P 2S P T P Pog EY p POQEY P o free Q P Pp
13. l semantics That is for all CCSP clock closed terms P regions r and invariants p the following holds RT P r 1 7 R P 1 1 where r R P r 1 denotes the set of traces of the region automaton correspond ing to process P under the given starting conditions One can easily expect the above result since we have modelled the trace semantics on region automata but it is still important as it allows us to per form model checking of refinement relations using the operational model as for CSP Ros94 4 2 Extending the Semantics Failures Having defined the semantic model for region traces the next natural step is to extend it to a finer semantics that distinguishes between stable failures We define region failures again having in mind the operational model of region automata A region refusal set F is a subset of X U AU 2 and it describes the set of actions that a process can refuse after a given trace The most interesting case happens when a process refuses a delay action it means that it refuses to let time elapse this is useful to describe timed liveness properties A region failure is a pair t F where t is a region trace and f is a refusal set We denote by RFailures the set of region failures Following the same ideas described above for region traces we obtain a new semantic model for Clocked CSP processes given by a RegionF ailures function which is once again congruent with the operational model and a new refine
14. ment relation ERF 5 Model Checking Clocked CSP At first the semantics we have given does not seem very useful one of its main disadvantages is that it makes explicit references to clock names syntactic en tities in the notion of trace and failure In this way it distinguishes too much as it is shown in the following example the processes P x a x 1 gt xh a x 1 SKIP P gt x a 1 gt a x 2 SKIP would be distinguished as P resets clock x twice while P gt does it only once Clearly we would like to identify the two processes they are timed bisimilar How can we overcome this problem The first trivial step is to define refine ment up to clock renaming Next we have to define a way to verify interesting timed properties To do this consider the trace model and note that if we hid clock actions either resets or delays from traces we would be able to verify functional untimed refinement If we hid only some of them then we would be able to verify the refinement with respect to only a subset of clocks possibly the subset that describes the timed behaviour that we are interested in We describe the idea by means of an example also used in OW02 Assume that we want to check if a process respects the bounded invariance property a 17b where I 0 n is a closed interval starting from 0 This means that whenever an action a is performed the process cannot
15. no difference in our case because we use no relations based on the labelled transition system e g timed bisimulation if we did existing results might not hold but it would not be difficult to generalise the notions to ignore clock reset actions The transition system defined above has an infinite continuous set of states and actions in order to be able to model check timed automata we discretise such state space into several equivalence classes that relate clock valuations that agree on the integral part of clocks and on the ordering of their fractional part Let cy be the greatest constant against which clock x is compared x the integral part of x and fr x its fractional part Given a set of clocks C two clock valuations v and v are equivalent v c v if all of the following conditions hold for all x E C v x v x or they both exceed cz for all z y C with v x lt cs and v y lt cy fr v x lt fr v y if fro 2 lt fr for all x C with v x lt cz fr v x 0 if fr v x 0 A clock region is an equivalence class induced by and the region graph is the set of equivalence classes Since all valuations in the same region agree on the integral parts of the clocks it is clear that the same set of action transitions can be enabled from within the region We denote the set of regions associated to a timed automaton A by Ry and we let r r1 r2 range over regions We al
16. nt respectively deadlock successful termination action prefix internal choice external choice interface parallel hiding renaming recursion and sequential composition The semantics of a CSP term P is given by the set of actions that it can perform traces by the set of actions that it can refuse after a possible trace failures or by its possible infinite executions divergences Different relations are built upon these semantic models for each of them equivalences between processes are defined as set equalities CSP also introduces the idea of refinement a process P is refined by another process P gt P E P 2 if every behaviour of P is a possible behaviour of P that is if it is less deterministic This idea is formally defined as inverse set inclusion of traces failures or divergences For a detailed introduction to CSP see introductory texts e g Ros98 or Sch99 3 Clocked CSP We define a language for describing timed automata called Clocked CSP CCSP as an extension of CSP thus keeping its choice operators the hiding operator and the multi way parallel composition Clocked CSP terms with alphabet X and set of clocks C are obtained by the following syntax P STOP SKIP a gt P mP XP POP POP P P up P P A P P A where a X A C X 6 B C and X C C By convention actions will be ranged over by a b clocks by z y sets of clocks by X Y and cloc
17. of regions corresponding to a term and 1 2 m the set of possible invariants note that this set is finite as an invariant is the union of a set of regions We define a function RT CCSP x RxT RTraces that returns the region traces of a process starting from a par ticular region under a particular invariant The semantics of a process is given by an ordered set of sets of traces RegionTraces P RT P Ti 1 RT P Ti 2 pecs RT P Ti Pm RT P Trn p1 RT P Tn 2 Pere RT P Tn Pm The function RT is defined inductively on the syntax of terms along the same lines as the definitions of the rules for traces for classical CSP We can then extend the refinement relation as reverse inclusion of behaviour P Err Q iff RegionTraces P 2 RegionTraces Q that is for every possible starting region Q s behaviour is a subset of P s be haviour It can be shown that the refinement relation is independent of the starting conditions for processes that reset all their clocks before referencing them in this way only one set inclusion needs to be verified Moreover we usu ally consider refinements between processes that have no external clocks so that their behaviour is self contained Theorem 1 RegionTraces is a monotonic function with respect to all the op erators and the fixed point operation is well defined for guarded processes Theorem 2 The function RT is a congruence with respect to the operationa
18. real time in more details References ACD93 R Alur C Courcoubetis and D L Dill Model checking in dense real time Information and Computation 104 1 1 34 1993 AD91 R Alur and D Dill The theory of timed automata In J W de Bakker C Huizing W P de Roever and G Rozenberg editors Proceedings of the REX Workshop Real Time Theory in Practice volume 600 pages 45 73 1991 D A99 P R D Argenio Algebras and Automata for Timed and Stochastic Sys tems PhD thesis Department of Computer Science University of Twente November 1999 DJR 92 J Davies D Jackson G Reed J Reed A Roscoe and S Schneider For93 Hoa85 Jac92 LPY97 Mil89 Oua01 OW02 Ros94 Ros98 RR86 Sch97 Sch99 Yov96 Yov97 YPD94 Timed csp Theory and practice In Proceedings of REX Workshop Ni gmegen LNCS 600 Springer Verlag 1992 1992 Formal Systems Europe Ltd Failures divergence refinement user manual and tutorial 1993 Version 1 3 C A R Hoare Communicating Sequential Processes Prentice Hall Interna tional Englewood Cliffs 1985 D M Jackson Logical Verification of Reactive Software Systems PhD thesis University of Oxford 1992 Kim G Larsen Paul Pettersson and Wang Yi UPPAAL in a Nutshell Int Journal on Software Tools for Technology Transfer 1 1 2 134 152 October 1997 R Milner Communication and Concurrency Prentice Hall International Englewood Cliffs
19. so often denote a region by the set of clock constraints that are met by the valuations in the region only Finally we denote by r the starting region all clocks set to 0 and by rmax the region for which x gt c for all clocks z With passage of time the automaton changes region Intuitively we define the successor region as the next region that the system will be in by letting time elapse Formally the successor region is a function succ R gt R such that succ r r if for all v r there exists d R such that v d succ r and for all d lt d either v d v or v d succ r succ is undefined for rmaz The action of moving to the next region involves an increment of the value of all clocks but only some of them actually cause the change of a region For example if we consider two clocks x and y when going from the region x y 0 to the region 0 lt x y lt 1 both clocks change region On the contrary when going from 0 lt x lt 1 A y 0 to 0 lt a lt 1AO lt y lt 1LAly lt x it is only y that changes region We are interested in identifying the set of clocks that change their own region as it will be convenient in the following We define clocks R 2 as the set of clocks that change their own region at the next succ action clocks r is the smallest set X of clocks such that for all valuations v r and succ r we have v c x n We also define A as the set of actions descri
20. sult of the parallel or external choice operators one of them can reset a clock thus affecting the behaviour of the other process As an example consider the following process P jz a x gt 1 STOP Q b tt gt z a tt STOP R PO Q d It is possible for process Q to reset the clock x after P has reset it and started waiting for the guard x gt 1 to become true So the behaviour of P is influenced by Q s internal actions and it is not possible to define P s semantics without knowing the context placing some restrictions on the processes and modifying the semantics To avoid such problems it was necessary to impose several constraints on the syntax Our choice was to model the semantics on the region automaton In the next section we describe the trace semantics obtained by modelling region automata In the later sections we discuss advantages and disadvantages of our approach 4 A Trace Semantics In order to obtain compositionality we have to impose restrictions on processes Since the interaction between processes that modify the value of clocks is what creates most problems we make the following simplification each process can handle only some clocks so that its behaviour depends only on them The P 4P T P y P 2 P T P _ K P 0 P Q apno pP P Q Teng p Q P 25 P I P g K P 40 Pog P Table 3 New operational r
21. to use FDR2 to verify properties of processes in the extended CSP and refinement relations This paper is structured in the following way in Section 2 we give the back ground notions on timed automata and CSP needed to understand the rest of the paper in Section 3 we introduce the extended language Clocked CSP we give it an operational semantics and discuss the issues concerning a CSP style denotational semantics the denotational model for traces is described in Sec tion 4 giving highlights of its extension to failures Section 5 describes how it is possible to use Clocked CSP to verify properties of processes with FDR2 Fi nally in Section 6 we discuss the advantages and disadvantages of our approach and future work 2 Preliminaries Timed Automata Given a set C of real valued variable called clocks the set B C of clock constraints is generated by the following grammar gu auK lt cla y lt c dA d n7d for x y E C xE lt lt and c N Given a clock constraint we define vars to be the set of clocks appearing in the constraint Definition 1 A timed automaton A is a tuple L 1 2 C Z where L is the set of locations l is the initial location X is the set of actions or alphabet C is the set of clocks T L B C is location invariant function k L 2 is the set of resets and gt C Lx X x B C x L is the set of edges We 3 ad write s gt s whenever s a 8 E gt A timed automa
22. ton is given a semantics in terms of a labelled transition system At each point of the computation one must know the location the system is in and the current value of clocks So the state space of the transition system is given by the cross product of locations and clock valuations Formally a clock valuation v for a set of clocks C is a function v C gt Rt that assigns a positive real value to each clock The semantics of a timed automaton is given by the labelled transition system LTS Q q X UR s defined as follows Q is the set of states A state is a pair l v where l LU free L and v is a clock valuation free L is an additional set of locations for which the set of clock resets is empty that is free 1 0 the starting state is l vo where vo is the valuations that assigns 0 to all the clocks 1sC Qx SURU2 x Q is the set of transitions the smallest set respecting the rules of Table 1 Action 14S vj Kl 0 L v Sus l v Reset T Mrs iv us Freel vik N Yd lt d v d EI l K 0 Lv Sous Lv a Table 1 Transition relation of the labelled transition systems associated to a timed automaton The definition we have given is different from the one usually in the literature since we consider clock resets as external actions The reason for this will become clear later when we give semantics to our language and we want clock reset to be visible this makes
23. ules for external choice other clocks are used by other processes that interact with it through the parallel operator More formally for each process or timed automaton the set of clocks C is partitioned into the set of internal clocks Cr and the set of external clocks Cp We restrict the parallel operator to work only on processes with distinct sets of internal clocks The idea behind this is that when defining the semantics of a term we have to assume any possible action on external clocks by the other processes that is a process must be willing to synchronise on any possible set of external clock reset at any moment In this way processes always agree on the value of clocks This is the reason why we treat clock resets as visible actions when a process resets a set of clocks X the other processes are willing to synchronise on this reset actions and in this way they know what the other processes are doing We believe this is a reasonable restriction since in most examples involving timed automata we have seen the requirement that parallel components use disjoint sets of clocks The other critical operator is external choice since processes involved can take internal actions and then reset some clocks thus modifying the behaviour of the other component This is another reason why we treat clock resets as external actions that can resolve the choice Informally the idea is that when presenting the environment a choice we present
24. urs allows us to verify whether a process implements a specification in this way implementations can be further refined allowing for chains of refinements leading toward the final implementation CSP has been the subject of extensive research and most notably it has an effective associated software tool FDR2 For93 that can automatically verify refinement relations Traditional process calculi can only verify functional properties of systems that is properties that are not time sensitive More recently substantial effort has been directed to describe systems and their timed behaviour in order to verify their real time properties consequently extending existing models There are proposals to extend CSP to describe real time systems The most important is Timed CSP RR86 DJR 92 Much work has been done since its introduction Supported by EPSRC grant GR N22960 but it has never had much success mainly because of the lack of successful verification algorithms The main difficulty with Timed CSP and most real time systems with a continuous representation of time is that their behaviour is infinite and continuous making them hard to analyse There are two main techniques that have been proposed to automatically verify Timed CSP one is the timewise refinement Sch97 Sch99 the other is digitisation Oua01 The idea behind timewise refinement is to ignore time and to verify only functional properties of a Timed CSP process This is done
Download Pdf Manuals
Related Search