Specification and Verification of Synchronizing Concurrent Objects
Gabriel Ciobanu and Dorel Lucanu
“A.I.Cuza” University of Ia¸si, Faculty of Computer Science {gabriel, dlucanu}@info.uaic.ro
Abstract. We introduce a new specification formalism which we call hiddenCCS; hidden algebra is used to specify local goals as objects, and CCS is used to describe global goal of the synchronizing concurrent ob- jects. We extend the object specification with synchronization elements associated with methods of different objects, and we use a CCS coor- dinating module to describe the interaction patterns of methods invo- cations. Some results refer to strong bisimulation over the hiddenCCS configurations. We investigate how the existing tools BOBJ, CWB, and Maude can be integrated to describe and verify useful properties of the synchronizing concurrent objects. The hiddenCCS specifications can be described in the rewriting logic using Maude. Finally we present the first steps towards temporal specifications and verification for hiddenCCS.
Keywords:algebraic specification, integration, concurrent systems, object- oriented specification, hidden algebra, CCS, temporal logics, model checking.
1 Introduction
The complexity and dynamic interaction of software components provide chal- lenging research issues in large system design and verification. Although some specification techniques can support concurrent interaction, they generally can- not scale up for modeling the data and state of complex distributed systems. On the other hand, state-based formalisms such as hidden algebra provide specifica- tion techniques for capturing complex data and states; however, they are weak for capturing the interaction aspects of concurrent systems. A possible approach is to integrate two specification techniques. In this paper we investigate the in- tegration between hidden algebra and CCS, introducing a powerful specification technique which we callhiddenCCS. We use this name to express that we deal with objects specified inhiddenalgebra, and their interactions are described by CCSprocesses.
The new formal model for concurrent objects is able to capture the relevant dynamics (operational semantics) of the whole system, allowing derivation of
This paper was partially written in June 2003 while the second author has visited National University of Singapore within the EERSS Programme.
the system properties from those of its objects and model checking tools. The symbiosis of object-oriented algebraic specification and interaction process alge- bra is given by a simple formal glue provided by some synchronization elements added to hidden algebra and appropriate semantic rules. HiddenCCS extends object-oriented hidden algebra with a CCS coordinating module able to de- scribe the interaction patterns of method invocations. From an object-oriented point of view, we preserve the properties and the expressive power of hidden algebra specification and its hidden logic. From a process algebra point of view, we describe the possible patterns of interaction between objects and preserve the expressive power of CCS and its Hennessy-Milner logic.
Hidden algebra takes as basic the notion of equational behavioral satisfac- tion: this means that hidden specifications characterize how objects behave in response to a given set of experiments. Hidden algebra is able to handle the most troubling features of large systems, including concurrency, nondeterminism, and local states, as well as the usual features of the object paradigm, including classes, subclasses (inheritance), attributes and methods, in addition to logical variables, abstract data types, and generic modules [7].
CCS is a calculus used to specify how the interactive systems should behave.
A CCS process expresses the interaction between subsystems as well as the capability of the system to interact with other systems running concurrently.
We may think that a CCS process describes communication scenarios which the designed system should be able to perform. Therefore we use CCS to specify the communication requirements.
We extend the algebraic specification with synchronization elements simi- lar to CCS communication channels; such a channel links the object initiating a method invocation and the corresponding object method. The formal opera- tional semantics of hiddenCCS integrates state transition semantics of hidden algebra and CCS reduction rules by using these synchronization elements. In this way we provide a foundation for complex derivations, and a reasoning system by combining hidden logic and Hennessy-Milner logic. This new specification technique is very flexible, allowing the reuse of both object specifications and coordinating CCS module.
The structure of the paper is as follows. Section 2 presents hidden algebra and BOBJ. Section 3 recalls the main definitions of CCS. In Section 4 we in- troduce the new hiddenCCS specifications, and present some theoretical results.
Section 5 presents the existing software tools for CCS and hidden algebra, pre- senting Maude as a software framework able to handle hiddenCCS specifications.
The first steps towards temporal specifications for hiddenCCS are presented in Section 6. Conclusion and references end the paper.
2 Specification of Objects in Hidden Algebra
We assume that the reader is familiar with algebraic specification. A detailed presentation of hidden algebra can be found in [7, 13]. Here we briefly reiterate the main concepts and notations.
A(fixed data) hidden signatureconsists of two disjoint sets:V ofvisiblesorts, and H ofhidden sorts; a many sorted (V ∪H)-signatureΣ; and an ΣV-algebraD calleddata algebra. Such a hidden signature is denoted byΣ, and its constituents are denoted byH(Σ),V(Σ), and D(Σ) respectively. Given a hidden signature (V, H, Σ, D), a hidden Σ-model is a Σ-algebra M such that MΣV= D. This means that the interpretation of each sort s ∈ V ∪H is a distinct set Ms, and the interpretation of a symbol f ∈ Σs1···sn,s is a function [[f]]M : Ms1 ×
· · · ×Msn → Ms. By MΣV we denote the algebra M restricted only to the visible sorts and visible operations. Ahidden Σ-homomorphism h:M →M is a Σ-homomorphism such thathΣV= idD.
Given a hidden signature (V, H, Σ, D) and a subsignatureΓ ⊆Σ such that ΓV=ΣV, a Γ-context for sort sis a term in TΓ({ :s}
Z) having exactly one occurrence of a special variable of sort s.Z is an infinite set of distinct variables.CΓ[ :s] denotes the set of allΓ-contexts for a sorts. Ifc∈ CΓ[ :s], then the sort of c, seen as a term, is called the result sort of the contextc. A Γ-context with visible result sort is called a Γ-experiment. If c∈ CΓ[ :s] with the result sorts andt∈ TΣ(X)s, thenc[t] denotes the term inTΣ(var(c)∪X) obtained fromcby substitutingt for . Furthermore, for each hidden Σ-model M,c defines a map [[c]]M :Ms→[Mvar(c)→Ms] given by [[c]]M(a)(ϑ) =aϑ(c), where aϑ(c) is the variable assignment{ →a} ∪ {z→ϑ(z)|z ∈var(c)}. We call [[c]]M theinterpretationof the contextcin M.
Given a hidden signature (V, H, Σ, D), a subsignature Γ ⊆ Σ such that Γ V= ΣV and a hidden Σ-model M, the Γ-behavioral equivalence on M, denoted by≡ΓΣ, is defined as follows: for any sorts∈V∪H and anya, a ∈Ms,
a≡ΓΣ a iff [[c]]M(a)(ϑ) = [[c]]M(a)(ϑ)
for allΓ-experimentscand all (V ∪H)-sorted mapsϑ:var(c)→M.
Given an equivalence ∼ onM, an operation f ∈Σs1...sn,s is congruent wrt ∼ iff [[f]]M(a1, . . . , an)∼[[f]]M(a1, . . . , an), wheneverai ∼ai for i= 1, . . . , n. An operationf ∈ΣisΓ-behaviorally congruent wrtM iff it is congruent wrt≡ΓΣ. A hidden Γ-congruenceonM is a (V∪H)-equivalence onM which is the identity on visible sorts and each operation inΓ is congruent with respect to it.
Theorem 1. [7, 13] Given a hidden signature(V, H, Σ, D), a subsignatureΓ ⊆ Σsuch thatΓV=ΣV and a hiddenΣ-modelM, thenΓ-behavioral equivalence is the largest hidden Γ-congruence onM.
Given aΣ-equationeof the form (∀X)t=t ifC, a hiddenΣ-modelM Γ- behaviorally satisfiese if and only if for allϑ:X →M, ϑ(t)≡ΓΣ ϑ(t) whenever ϑ(u)≡ΓΣ ϑ(v) for allu=vinC. We writeM |≡ΓΣ e. IfE is a set ofΣ-equations, then we writeM |≡ΓΣ E iffM |≡ΓΣ efor allein E.
Abehavioral specificationis a tripletB= (Σ, Γ, E) consisting of a hiddenΣ- signature, a subsignatureΓ ⊆Σsuch thatΓV=ΣV and a set ofΣ-equations.
We often denote the constituents ofBbyΣ(B), Γ(B) and respectivelyE(B). The elements of Γ \(ΣV) are called behavioral operations. A hidden Σ-model M behaviorally satisfiesthe specificationBiffM Γ-behaviorally satisfiesE, that is M |≡ΓΣ E. We writeM |≡ B and we say that M is aB-model. For any equation
e, we writeB |≡eiffM |≡ BimpliesM |≡e. An operationf ∈Σisbehaviorally congruentwrtBifff isΓ-behaviorally congruent wrt eachB-modelM.
Behavioral specifications can be used to model concurrent objects. The frame- work for simple objects is the monadic fixed-data hidden algebra [13]:Bspecifies a simple objectiff
1.H(B) has a unique elementhcalledstate sort;
2. each operationf ∈Σ\ΣV is either:
– a hidden (generalized) constant modeling an initial state, or – amethod g:hv1· · ·vn→hwithvi∈V fori= 1, . . . , n, or
– anattributeq:hv1· · ·vn→v withv∈V andvi ∈V fori= 1, . . . , n.
A concurrent connection B1 · · · Bn is defined as in [8] where the composite state sort is implemented as tupling. If hi is the state sort of Bi, then a com- posite state is a tuplest1, . . . , stn:Tuplewhere the statesti is of sorthi. For i = 1, . . . , n, the projection operations i∗ are defined by projection equations i∗(st1, . . . , stn) = sti, together with “tupling equation”1∗st, . . . , n∗st =st for eachstof sortTuple.
We assume that all specificationsB1, . . . ,Bnshare the same data algebra. For each componentBi andf in Bi, we further consider an operationf.Bi defined by:
f.Bi(st1, . . . , stn,−→x) =f(sti,−→x) iff is an attribute, and
f.Bi(st1, . . . , stn,−→x) =st1, . . . , f(sti,−→x), . . . , stniff is a method, where by−→x we denote a sequence of the formx1, . . . , xn.
Proposition 1. [7] 1. Iff is a method ofBi,g a method ofBj, andi=j, then f.Bi(g.Bj(st,−→y),−→x) =g.Bj(f.Bi(st,−→x),−→y)
2. Iff is an attribute ofBi,g a method ofBj, andi=j, then f.Bi(g.Bj(st,−→y),−→x) =f.Bi(st,−→x).
The first part of Proposition 1 allows us to consider the methodf.Bi g.Bj
such that f.Bi g.Bj(st,−→x ,−→y) means the concurrent execution of f.Bi(st,−→x) and g.Bj(st,−→y). If f.Bi andg.Bj are in Γ, then f.Bi g.Bj is inΓ as well. The second part says that the components do not share memory. The shared memory can be modeled as a distinct object and the synchronization is realized by the mechanism described below. Note that the new added functions f.Bi could be non-behavioral inB even iff is behavioral inBi.
By object specification we mean either a simple object specification, or a conservative extension of a concurrent connection of object specifications. We extend an object specification by adding elements of synchronization given by pairs (a, a) denoting the necessity and availability of a shared name a. Let Synch(B) denote the set of the synchronization elements of B. Both a and a can be associated with behavioral methods of different objects; the invocation of these methods expresses the necessity and the availability ofa, respectively. Let synch(g) =adenote the fact that the nameais associated with the methodg.
An elementais calledclosed synchronization forB iff bothaandaare present in B. If only one (eithera or a) is present in B, then it is called an open syn- chronizationforB.
The BOBJ system (http:://www.cs.ucsd.edu/groups/tatami/bobj/) is used for behavioral specification, computation, and verification. BOBJ extends OBJ3, supporting behavioral specification and verification, and in particular, providing circular coinductive rewriting with case analysis for conditional equations over behavioral theories. Like OBJ3, BOBJ supports ordinary rewriting for order sorted equational logic (modulo attributes), as well as first order parameterized programming. BOBJ is written in Java and so it can run on a wide range of platforms. We enrich the BOBJ syntax by adding the capability of declaring the elements of synchronization. We present two examples inspired by [12].
Example 1. Agency
An agent is working on an assembly line. He receives jobs on a conveyor belt represented by the port i, and dispatches them after assembly along another conveyor belt represented byo. A job can be easy, neutral, or difficult. Here we consider a system consisting of two concurrently working agents. We start by specifying the data algebra:
dth DATA-AGENT is
sorts JobGrade ErrJobGrade . subsort JobGrade < ErrJobGrade . ops easy neut diff : -> JobGrade . op none : -> ErrJobGrade .
end
An agent is specified as a simple object:
bth AGENT is sort Agent . pr DATA-AGENT .
op easyJob : Agent -> Agent [synch: iE] . op neutJob : Agent -> Agent [synch: iN] . op diffJob : Agent -> Agent [synch: iD] . op endJob : Agent -> Agent [synch: ~o] . op grade : Agent -> ErrJobGrade .
var A : Agent .
eq grade(endJob(A)) = none . eq grade(easyJob(A)) = easy . eq grade(neutJob(A)) = neut . eq grade(diffJob(A)) = diff . end
The attributes of the formsynch: iEare new; they do not appear in the stan- dard definition of BOBJ, and they specify the synchronization elements associ- ated with the respective methods. Generally, a method having such an attribute is concerned with the availability or the necessity of some resource. The notation o is represented in BOBJ by ~o. The whole system is given by the concurrent connection of two agents:
bth AG1 is pr AGENT * (sort Agent to Agent1) . end bth AG2 is pr AGENT * (sort Agent to Agent2) . end bth AGENCY is
pr (AG1 || AG2) * (sort Tuple to Agency) . end
Example 2. Job Shop.
We refine the agency example by adding a hammer and a mallet to the system.
A difficult job can be done only with the aid of the hammer, and a neutral job can be done only with either the hammer or the mallet. Obviously, the hammer and the mallet are shared by the two agents. We first refine the specification of an agent by adding the ability to get/release the hammer/mallet.
bth AGENT is inc AGENT .
op getHammer : Agent -> Agent [synch: ~gh] . op putHammer : Agent -> Agent [synch: ~ph] . op getMallet : Agent -> Agent [synch: ~gm] . op putMallet : Agent -> Agent [synch: ~pm] . eq grade(getHammer(A)) = grade(A) .
eq grade(putHammer(A)) = grade(A) . eq grade(getMallet(A)) = grade(A) . eq grade(putMallet(A)) = grade(A) . end
The hammer and the mallet are specified as follows:
bth HAMMER is sort Hammer .
op alloc : Hammer -> Hammer [synch: gh] . op release : Hammer -> Hammer [synch: ph] . op isAv : Hammer -> Bool .
var H : Hammer .
eq isAv(alloc(H)) = false . eq isAv(release(H)) = true . end
bth MALLET is sort Mallet .
op alloc : Mallet -> Mallet [synch: gm] . op release : Mallet -> Mallet [synch: pm] .
*** the rest is similar to HAMMER end
In this example the synchronization elements are gh, ph, gmand pm.AG1and AG2are using the new definition for AGENT. The new system is specified as the concurrent connection of the two agents, together with the hammer and the mallet:
bth JOBSHOP is
pr (AG1 || AG2 || HAMMER || MALLET) * (sort Tuple to Jobshop) . end
It is not clear how the agents coordinate their activities for a correct use of the resources. Their interaction is specified later by adding a CCS coordinating module.
Hidden logic[13] is a generic name for various logics strongly related to hid- den algebra offering sound rules for behavioral reasoning which can be easily automated. BOBJ supports hidden logic by implementing behavioral rewriting, circular coinductive rewriting, automatic cobasis generation, and concurrent con- nection. Here is a sample showing how BOBJ supports hidden logic:
BOBJ> select AGENT . BOBJ> show cobasis . The cobasis for Agent is:
op grade : Agent -> ErrJobGrade BOBJ> op init : -> Agent .
BOBJ> eq grade(init) = none .
BOBJ> cred init == endJob(easyJob(init)) .
==========================================
c-reduce in AGENT : init == endJob(easyJob(init)) using cobasis for AGENT:
op grade : Agent -> ErrJobGrade
--- result: true
BOBJ> select AGENT .
==========================================
The cobasis is used for proving behavioral equivalence by coinduction [13]. For our AGENT specification, two states A and A are behaviorally equivalent iff grade(A) =grade(B). Then we define a new state init with grade(init) = none, and we prove that init and endJob(easyJob(init)) are behaviorally equivalent.
3 Calculus of Communicating Systems
The Calculus of Communicating Systems (CCS) was originally developed by Milner in 1980, and supports the synchronization of interacting processes [11].
CCS provides a minimal formal framework to describe and study synchroniz- ing concurrent processes and various behavioral equivalences. Interaction among processes is established by a matching between complementary ends aandaof an arbitrary synchronization channel a. When there are many pairs which can satisfy the matching condition, only a single pair (a, a) is selected.
We assume a set A of names; the elements of the set A = {a | a ∈ A}
are called co-names, and the elements of the set L =A∪A are labels naming ordinary actions. The function a→ais extended to L by defininga=a. The standard definition of CCS includes only one special action calledsilent action and denoted byτ, intended to represent the internal synchronization of a system.
Theprocessesare defined over the setAof names by the following syntactical rules [12]:
P ::= 0 | α.P | P+Q | P|Q | newL P | Aa1, . . . , an
whereP andQrange over processes,αover actions,ai over names, andAover the process identifiers.
A structural congruence relation is defined over the set of processes. The relation≡over the set of processes is calledstructural congruence, and is defined as the smallest congruence which satisfies:
– P≡QifQcan be obtained fromP byα-conversion – P+ 0≡P,P+Q≡Q+P, (P+Q) +R≡P+ (Q+R), – P|0≡P,P |Q≡Q|P, (P|Q)|R≡P |(Q|R).
The structural operational semantics is shown in Figure 1, where we have already assumed that the summation and parallel composition are associative and commutative. If −→a = (a1, . . . , an) and −→
b = (b1, . . . , bn), then {−→b/−→a}P denotes the renaming construction P[b1/a1, . . . , bn/an]. We also assume that every process identifier A has a defining equation of the form A(−→a) def= PA wherePA is a summation of processes, and−→a includes all the free names inPA.
α.P −→α P
P −→α P P+Q−→α P P−→α P
P|Q−→α P|Q
{−→b/→−a}PA−→α P A−→
b−→α P
A(−→a)def=PA
P−→α P
newL P −→α newL P α∈L∪L P −→α P Q−→α Q P|Q−→τ P|Q P −→τ∗P P−→α Q Q−→τ∗Q
P=α⇒Q
Fig. 1.CCS operational semantics rules
Strong bisimulation, written ∼, is defined over the processes as the largest symmetrical relation such that: ifP ∼QandP −→α P, then there existsQsuch that Q−→α Q andP ∼Q.
Weak bisimulation, written ≈, is defined over the processes as the largest symmetrical relation such that: ifP ≈QandP −→α P, then there existsQsuch that Q=α⇒Q andP ≈Q.
The following two examples show how it is possible to describe patterns of synchronization by using CCS expressions.
Example 3. Agency (continued).
The hidden specificationAGENCYdoes not include any constraint concerning the order in which the methods are executed. Using the synchronization elements, we use CCS expressions to describe scenarios followed by the two agents:
Adef= iE.B+iN.B+iD.B, Bdef= o.A Agencydef= A|A
Example 4. Job Shop (continued).
The hidden specification JOBSHOP say nothing about how the two agents are using the hammer and the mallet. We use CCS expressions to specify that two agents cannot use a tool at the same time:
Hdef= gh.H, Hdef= ph.H,M def= gm.M, Mdef= pm.M, Jdef= iE.JE+iN.JN +iD.JD,
JEdef= o.J,JN def=gh.ph.JE+gm.pm.JE,JDdef= gh.ph.JE J obShopdef=new gh ph gm pm (J|J |H |M)
The CCS specificationJ obShopdescribes a pattern of interaction that cannot be described in hidden algebra. It is possible to have various patterns of interaction between objects. For instance, a neutral job can use only the mallet and we have then: JN def= gm.pm.JE. In this way we get a clear concern separation: the local goals are given by the object specifications, and the global goal is given by the CCS coordinating process. In the next section we present the semantic integration of these two modules.
Hennessy-Milner Logic(HML) is a primitive modal logic of actions used for describing local capabilities of CCS processes. HML formulas are as follows:
ϕ::=tt|ff|ϕ1∧ϕ2|ϕ1∨ϕ2|[a]ϕ| aϕ|[[a]]ϕ| aϕ.
IfP is a CCS process andϕa HML formula, the satisfaction relation P|=ϕis inductively defined as:
P|=tt, P|=ϕ1∧ϕ2 iffP |=ϕ1 andP|=ϕ2, P |=ϕ1∨ϕ2 iffP|=ϕ1 orP |=ϕ2 P|= [a]ϕ iff (∀P∈ {P|P−→a P})P|=ϕ
P|=aϕ iff (∃P∈ {P|P −→a P})P|=ϕ P|= [[a]]ϕ iff (∀P∈ {P|P=a⇒P}) P|=ϕ P|=aϕ iff (∃P∈ {P|P=a⇒P})P|=ϕ
Example 5. Agency (continued).
Here are two examples of HML formulas satisfied by the agent processes:
A|=iEtt∧ iNtt∧ iDtt, B|=ott
4 HiddenCCS Specifications
The integration of CCS and object specification in hidden algebra is given by the elements of synchronization. A CCS process over the elements of synchronization works as a coordinating module that manages the interaction between object components. In our formalism, we provide structure to the CCS actions, and it is enough to consider the pure CCS to model the synchronization between distributed objects. The synchronization elements are provided by pairs (a, a) with each component associated with a method; in this way we have a method- method interaction. We extend this approach in [1] by adding communication between objects.
AhiddenCCS specificationis a triple (B,P,IC) consisting of an object spec- ification B given in hidden algebra, a CCS description P of the coordinating module, and a setIC of integration consistency requirements. The semantics of hiddenCCS specifications is given by a labeled transition system defined over configurations (hidden state, CCS process) as follows:
1. IfP −→α P, then (st, P)−→α (st, P) wherestis obtained fromstby applying the method designated byα.
2. IfP −→α P,Q−→α Q, andαis closed, then (st, P |Q)−→τ (st, P|Q) where st is obtained from st by synchronously applying the methods designated byαandαwhenever integration consistency requirements are satisfied. For instance, the synchronous application of the methodsgetHammerandalloc, corresponding to the synchronization given byghandgh, is possible only if isAv.HAMMER(st) =isAv(3∗st) =true.
This definition is sound if each (co-)name is uniquely associated to a method.
Whenever the same name a is related to more than one method, e.g. to the methodsg1, . . . , gn, then we considerndistinct copiesa1, . . . , an of the namea, each of them for the corresponding method. Moreover, we define a relation eq given byaieqafori= 1, . . . , n. The operational semantics of CCS is modified as follows. The “synchronization” rule is replaced with:
P −→αi P Q−→αj Q
P|Q−−−−−→τ(αi,αj) P|Q αieqαandαjeqα
For the silent action τ we use a more exact notation τ(αi, αj) indicating the names involved in such an internal action. This notation is necessary to inte- grate CCS semantics with the behavioral semantics of hidden algebra. Since τ is used in the definition of the CCS bisimulation, the following rules restore it fromτ(αi, αj), whereα∗=if (α=τ(αi, αj)) then τ else α:
P −−−−−→τ(αi,αj) Q P=τ⇒Q
P=τ⇒∗P P−→α Q Q=τ⇒∗Q P =α⇒∗ Q
A CCS(B)-process is a CCS process built over the set Synch(B). An integra- tion consistency requirement expresses the availability of a synchronization re- source and consists of a finite set of equations q( , d1, . . . , dn) =d, where q is an attribute in Γ and d, d1, . . . , dn ∈ D(B). Let ic(αi, αj) denote the integra- tion consistency requirement corresponding to the synchronization pair (αi, αj), whereαieqαandαjeqα. A statestof a modelM satisfiesic(αi, αj) whenever [[q]]M(st, d1, . . . , dn) =dfor each equationq( , d1, . . . , dn) =d ofic(αi, αj); we writest|=ic(αi, αj).
Given an object specification B and a hidden B-model M, we denote by LT SΓ,CCS(M) the labeled transition system defined by the rules of Figure 2, where P, P, andQ, Q are CCS(B)-processes. Ifst is a state inM andP is a CCS process, then LT SΓ,CCS(M, st, P) denotes the subsystem induced by the subset of the configurations which are reachable from (st, P).
InLT SΓ,CCS(M) we have three types of transitions: those corresponding to open synchronizations (labeled byα=synch(g)), those corresponding to closed synchronizations (labeled by τ), and those corresponding to non-synchronizing behavioral methods (labeled byidle).
Definition 1. Let Σbe an object signature,Γ a hidden subsignature ofΣ, and letM andM be two Σ-models. The relationΣ,ΓM,M ⊆Mh×Mh is defined by:
stΣ,ΓM,M st iff[[q]]M(st, d1. . . , dn) = [[q]]M(st, d1. . . , dn) for any attributeq∈Γ,dl, . . . , dn∈D(B).
g:hi−→v →hi, synch(g) =α, st= [[g.Bi]]M(st,−→
d) P −→α P (st, P)−→α (st, P)
g:hi−→v →hi∈Γ non-synchronizing, st= [[g.Bi]]M(st,−→ d) (st, P)−−→idle (st, P)
g:hi−→v →hi, synch(g) =αi, g:hj−→v→hj, synch(g) =αj, st|=ic(αi, αj), st= [[g.Big.Bj]]M(st,−→
d ,−→
d), P −−−−−→τ(αi,αj) P (st, P)−→τ (st, P)
(st1, P) (−→ ∪τ −−→)idle ∗(st1, P) (st1, P)−→α (st2, Q) (st2, Q) (−→ ∪τ −−→)idle ∗(st2, Q) (st1, P)=α⇒(st2, Q)
Fig. 2.The transition systems associated with a hiddenCCS specification
Definition 2. Given an object specification B = (Σ, Γ, E), and two B-models M and M, then the behavioral CCS-based strong Γ-bisimulation between M andM is the largest relation ∼M,M such that (st1, P)∼M,M (st1, P)implies
1. st1Σ,ΓM,M st1,
2. if(st1, P)−→α (st2, Q), then there is(st2, Q)such that (st1, P)−→α (st2, Q)and(st2, Q)∼M,M (st2, Q), and 3. if(st1, P)−→α (st2, Q), then there is(st2, Q)such that
(st1, P)−→α (st2, Q)and(st2, Q)∼M,M (st2, Q).
Not all the configurations are acceptable for execution. For instance, a con- figuration (init,J obShop) is not acceptable ifisAv.HAMMER(init) =false, be- cause (init, J obShop) −→iD (st, P), st does not satisfy ic(gh,gh), andP re- quires this integration consistency. We say that a state st is consistent with a CCS processP iff for each configuration (st, P)∈LT SΓ,CCS(M, st, P),st sat- isfies the integration consistencies required byP. A ground termt of state sort isconsistentwith a processP iff [[t]]M is consistent withP for eachB-modelM. Proposition 2. Given an object specification B = (Σ, Γ, E), two CCS(B)- processes P andP, and two B-modelsM andM, thenP ∼P whenever there are st in M and st in M such that st is consistent with P, st is consistent with P, and(st, P)∼M,M (st, P).
Proof. Let us consider (st, P) ∼M,M (st, P) such that st is consistent with P and st is consistent with P. We have to show that P ∼ P. LetR be the relation defined byQ R Qiff there arest1andst1such that (st1, Q) is reachable from (st, P), (st1, Q) is reachable from (st, P), and (st1, Q) ∼M,M (st1, Q).
We show that ifQ1R Q1 andQ1−→α Q2, then there is Q2 such thatQ2 −→α Q2 andQ2R Q2. It follows thatR⊆ ∼.
Proposition 3. Given an object specificationB= (Σ, Γ, E)and a B-modelM, then(st, P)∼M,M(st, P)wheneverst≡ΓΣ st andP ∼P.
Proof. We define the relationRby (st, P)R(st, P) iffst≡ΓΣ standP ∼P. If (st, P)R(st, P) thenstΣ,ΓM,Mst, becauseΣ,ΓM,M is included in the behavioral equivalence. We show that if (st1, P1)R(st1, P1) and (st1, P1)−→α (st2, P2), then there are st2 and P2 such that (st1, P1) −→α (st2, P2) and (st2, P2)R(st2, P2).
ThereforeR⊆ .
The strong bisimulation∼M,M is able to avoid the experiments that are not meaningful from the interaction viewpoint. Since≡ΓΣ is not designed to do this, the converse of Proposition 3 is not generally true. Here is a counterexample.
Example 6. Buffer.
dth DATA is sort Data . inc NAT . subsort Nat < Data .
op err : -> Data . end
bth BUFF is sort Buff . inc DATA . op put : Buff Nat -> Buff [synch: in] . op del : Buff -> Buff [synch: ~out] . op get : Buff -> Data .
var N : Nat . var B : Buff . eq get(del(B)) = err .
eq get(put(B, N)) = N if get(B) == err . end
ConsiderΓ=Sig(BUFF) and the CCS processes Bdef= in.B,Bdef= out.B. If initis a state withget(init) = errandst = del(put(init,n), then init andstare not behaviorally equivalent, but we have (init, B)∼M,M (st, B) and (init, B)∼M,M (st, B) in anyBUFF-modelM. These two states are not behav- iorally equivalent because it may exist a model where the result of the experiment get(put(put( ,m),n)) is unpredictable, e.g.,get(put(put(init,m),n)) =nand get(put(put(st,m),n)) =err. This happens because the method put()is un- derspecified in the hidden specification BUFF. If we add the CCS coordinating module, then put() becomes completely specified in the resulting hiddenCCS specification since the CCS module allows only defined experiments [7] and it avoids repeatingput()actions.
Behavioral CCS-based strong Γ-bisimulation can be extended to different specifications related by signature morphisms.
Definition 3. Given two object specifications B=(Σ, Γ, E)andB=(Σ, Γ, E) withSynch(B) =Synch(B)andD(B) =D(B), a signature morphismφ:Σ→ Σ preserving behavioral operations and synch, a B-model M and a B-model M, then the behavioral CCS-based weakΓ-bisimulationbetween M and M is the largest relation ≈M,M such that(st1, P)≈M,M (st1, P) implies
1. st1Σ,ΓM,Mφst1,
2. if(st1, P)−→α (st2, Q), then there is (st2, Q)such that(st1, P)=α⇒(st2, Q) and(st2, Q)≈M,M(st2, Q), and
3. if(st1, P)−→α (st2, Q), then there is (st2, Q) such that(st1, P)=α⇒(st2, Q) and(st2, Q)≈M,M(st2, Q).
Example 7. Agency and Job Shop.
Letφbe the signature morphism φ:AGENCY→JOBSHOP,M anAGENCY-model, andM aJOBSHOP-model. Ifst is a state inM such that
[[grade.AG1]]M(st) = [[grade.AG2]]M(st) =none, andst is a state inM such that
[[grade.AG1]]M(st) = [[grade.AG2]]M(st) =none, then:
(st, A|A)≈M,M (st,new−→
t(J |J |H |M)) ([[diffJob.AG1]]M(st), A|B)≈M,M
([[diffJob.AG1]]M(st),new−→
t(J |JD|H |M)) ([[diffJob.AG1]]M(st), A|B)≈M,M
([[AG1.getHammer alloc.HAMMER]]M(st1),new−→t(J |ph.JE|H|M)) ([[diffJob]]M(st), A|B)≈M,M
([[putHammer release.HAMMER]]M(st2),new−→
t (J |JE|H|M)) wherest1= [[diffJob]]M(st),st2= [[getHammer.AG1 alloc.HAMMER]]M(st1).
Proposition 4. Let us consider two object specificationsBandBwithSynch(B)
=Synch(B) andD(B) =D(B), and a signature morphism φ:Σ(B)→Σ(B) preserving behavioral operations and synch. IfP is a CCS(B)-process, P is a CCS(B)-process, M is a B-model, and M is a B-model, then P ≈P when- ever there are st in M and st in M such that st is consistent with P, st is consistent withP, and(st, P)≈M,M (st, P).
Proof. Let us consider (st, P) ≈M,M (st, P) such that st is consistent with P and st is consistent with P. We have to show that P ≈ P. LetR be the relation defined byQ R Qiff there arest1andst1such that (st1, Q) is reachable from (st, P), (st1, Q) is reachable from (st, P), and (st1, Q) ≈M,M (st1, Q).
We show that if Q1R Q1 andQ1−→α Q2, then there isQ2 such thatQ2=α⇒Q2 andQ2R Q2. It follows thatR⊆ ≈.
5 Integrating the Existing Software Tools
5.1 Concurrency Workbench
The Concurrency Workbench(CWB) is an automatic verification tool for finite- state systems expressed in process algebra [4]. It is mainly an extensible tool for verifying systems written in the process algebra CCS. It provides different
methods, such as equivalence checking, model checking, simulation and abstrac- tion mechanisms for analyzing system behavior. Even though its utility has been demonstrated with several case studies, the impact on system design practice of such tools has been limited.
CWB supports the computation of numerous different semantic equivalences and preorders. It also includes a flexible model-checking facility for determining when a process satisfies a formula of an expressive temporal logic, namely the propositionalµ-calculus. CWB analyzes systems by converting their CCS speci- fications into finite labeled transition systems (LTS), and then invoking various routines on these LTSs. The CWB uses an ”on-the-fly” approach to construct LTSs from specifications, with transitions of components calculated and then combined appropriately into transitions for the composite system.
Suppose we have a CCS description of our Job Shop example that is stored in a file named jobshop.ccs. We present a session with the North Carolina CWB (http://www.cs.sunysb.edu/~cwb/):
cwb-nc> load jobshop.ccs
CWB builds an LTS modeling the behavior of each process, and thesizecom- mand displays the number of states and transitions of the LTS.
cwb-nc> size Jobshop States: 35
Transitions: 104
We can check whether Agency and J obshop are strong bisimilar (using eq -S bisim), or weak bisimilar (using simply eq). CWB tells that they are weak bisimilar, but they are not strong bisimilar.
cwb-nc> eq -S bisim Agency Jobshop ...
States: 40 Transitions: 126 FALSE...
Agency satisfies:
<iD>[t]ff Jobshop does not.
cwb-nc> eq Agency Jobshop States: 40
Transitions: 126 TRUE
When we enter the CWB simulator, we have various choices; typing the number of the selected choice, the simulation proceeded from there. This is similar to thesearchcommand in Maude. The random command lets the simulator make a certain number of random choices from those possible at every successive state in the simulation.
cwb-nc> sim Jobshop cwb-nc-sim> 1
(J | JD | H | M)\ {gh,ph,gm,pm}
1: -- t --> (J | ’ph.JE | BH | M)\ {gh,ph,gm,pm}
2: -- iD --> (JD | JD | H | M)\ {gh,ph,gm,pm}
3: -- iN --> (JN | JD | H | M)\ {gh,ph,gm,pm}
4: -- iE --> (JE | JD | H | M)\ {gh,ph,gm,pm}
cwb-nc-sim> 2
(JD | JD | H | M)\ {gh,ph,gm,pm}
1: -- t --> (’ph.JE | JD | BH | M)\ {gh,ph,gm,pm}
2: -- t --> (JD | ’ph.JE | BH | M)\ {gh,ph,gm,pm}
We can invoke the model checker to determine whether or not an agent satisfies a temporal formula. The currently supported temporal logics for the specification of formulas are theµ-calculus (which is the default) and GCTL. An option indi- cates that model-checking is to be on-the-fly, if possible. Global model-checking (if possible) is the default. However, global model-checking is not possible for GCTL formulas and is only available for alternation-freeµ-calculus formulas.
cwb-nc> chk -L gctl Jobshop "E F ~{-}"
Model checking completed.
FALSE, the agent does not satisfy the formula.
Execution time (user,system,gc,real):(0.080,0.000,0.000,0.113) cwb-nc> fd Jobshop
States explored: 35 No deadlock found.
Execution time (user,system,gc,real):(0.020,0.000,0.000,0.022)
The commandfdlooks for a deadlock of the system described byJ obShop.
5.2 Maude
Maude [3] is a system supporting both rewriting logic specification and compu- tation. Like BOBJ, Maude has been influenced by the OBJ3 language, which can be regarded as an equational logic sublanguage. Maude supports member- ship equational logic and rewriting logic computation, which are not supported by BOBJ. On the other hand, the current version of Maude does not support the hidden logic used by BOBJ for behavioral specification and verification. It has good properties as a general semantic framework for giving executable se- mantics to a wide range of languages and models of concurrency. In particular, it supports the representation of CCS and HML [16].
In this section we show that the transition system associated with a hid- denCCS specification can be naturally represented by a Maude rewrite specifica- tion. We first modify the Maude module implementing the operational semantics of CCS by replacing the rule for synchronization with the following two rules:
crl P | Q => {tau(L)}(P’ | Q’) if P => {L}P’ /\ Q => {~ M}Q’ /\ L eq M . crl P | Q => {tau(M)}(P’ | Q’) if P => {L}P’ /\ Q => {~ M}Q’ /\ L eq M . whereL eq Mrepresents the implementation of the eq relation. Then we change the definition ofτ, representing it by a function having as argument one of the actions involved in synchronization. This is not a restriction, because P | Q
τ(αi,αj)
−−−−−→ P |Q is the same as P |Q−−−→τ(αi) P |Q andP | Q−−−→τ(αj) P | Q. Moreover, we have τ(α) =τ(α).
Here is the Maude description of the CCS expressionJ obShop:
mod JOBSHOP-CCSPROC is inc CCS .
ops gh ph gh1 ph1 gh2 ph2 gm pm gm1 pm1 gm2 pm2 : -> Label . ops iE1 iN1 iD1 o1 iE2 iN2 iD2 o2 : -> Label .
ops H HH M MM J1 JE1 JN1 JD1 J2 JE2 JN2 JD2 : -> ProcessId . op JobShop : -> ProcessId .
eq gh eq gh1 = true . eq gh eq gh2 = true . eq ph eq ph1 = true . eq pm eq ph2 = true . eq gm eq gm1 = true . eq gm eq gm2 = true . eq pm eq pm1 = true . eq pm eq pm2 = true .
eq context = ( H =def gh . HH ) & ( HH =def ph . H ) &
( M =def gm . MM ) & ( MM =def pm . M ) &
( J1 =def iE1 . JE1 + iN1 . JN1 + iD1 . JD1 ) &
...
( JD2 =def ~ gh2 . ~ ph2 . JE2 ) &
( JobShop =def ( J1 | J2 | H | M)
\ gh \ gh1 \ gh2 \ ph \ ph1 \ ph2
\ gm \ gm1 \ gm2 \ pm \ pm1 \ pm2 ) . endm
gh1,gh2,ph1,ph2,gm1,gm2,pm1, andpm2are copies ofgh,ph,gm, and respec- tively pm corresponding to the two agents. Note that the operator newL P is represented by the restrictionP\L. We may use the Maude implementation of HML to verify properties of the CCS processes:
Maude> red ’JobShop.ProcessId |= < ’iE1.Label > tt .
reduce in MODAL-LOGIC : ’JobShop.ProcessId |= < ’iE1.Label > tt . result Bool: true
Maude> red ’JobShop.ProcessId |= < ’gh.Label > tt .
reduce in MODAL-LOGIC : ’JobShop.ProcessId |= < ’gh.Label > tt . result Bool: false
The module MODAL-LOGICdescribes HML. Since it is written at the metalevel, the CCS terms are quoted.
The current version of Maude does not yet support behavioral membership logic [10]. The price we pay is that we lose support for verification of the behav- ioral properties. Thesynchattributes and the rules in Figure 2 are used to build the rewrite rules. Here is (a sketch of) the Maude description of the hiddenCCS specification corresponding to the Job Shop example:
mod JOBSHOP-CCS is pr JOBSHOP-TEST . pr MODAL-LOGIC . sort CcsJobshop .
op <_‘,_> : Jobshop Term -> CcsJobshop . op 1*_ : CcsJobshop -> Jobshop .
op 2*_ : CcsJobshop -> Term . ...
crl [iE1] : < A, P > => < < easyJob(1* A), 2* A, 3* A, 4* A >, succ(P,’iE1.Label) >
if P |= < ’iE1.Label > tt . ...
crl [tau] : < A, P > => < < getHammer(1* A), 2* A, alloc(3* A), 4* A >, succ(P,’tau[’gh1.Label]) >
if P |= < ’tau[’gh1.Label] > tt /\ isAv(3* A) .
