Verification of message sequence charts

[0002] The invention relates generally to analyzing message sequence charts (MSCs) and more particularly to model checking systems modeled with high level MSCs.

[0003] Message Sequence Charts (MSCs) are commonly used to describe the executions of communication systems. An MSC describes messages passed between the participating concurrent processes in the system, abstracting away details such as program variables and their values. Different system executions or scenarios can be described using MSCs, providing a representation of different system features. Grouping together different scenarios is facilitated using high-level or hierarchical MSCs (HMSCs). These are graphs that include nodes and edges connecting the nodes, where each of the nodes references a single MSC. The graph structure allows for combining together scenarios and for describing execution alternatives according to the branches of the graph. This simple standard is particularly useful for specifying communication protocols.

[0004] Because HMSCs do not impose constraints on the number of sent but unreceived messages, HMSCs can describe infinite state spaces. For example, an HMSC can describe a system where a process can send infinite messages without receiving a message from any process in the system. The lack of constraints on sent but received message complicates the automatic verification of MSCs. Standard model checking methods, usually applied to finite state systems, cannot automatically verify an HMSC. For example, checking linear temporal logic (LTL) properties of HMSCs is undecidable. This result is discussed in R. Alur, M. Yannakakis, “Model Checking of Message Sequence Charts,” CONCUR'99, Concurrency Theory, LNCS 1664, Eindhoven, The Netherlands, 1999.

[0005] Checking LTL properties of HMSCs is based on the linearizations of the HMSCs. Linearizing an HMSC means completing the partial order between the events imposed by the HMSC's scenarios into total orders. In this approach, all the linearizations of an MSC execution satisfy the given LTL specification. Adding a bound on the number of messages in any communication channel permits translating HMSCs to finite state models that are exponentially larger than the original HMSC description. Standard model checking methods, like checking LTL properties, can then be applied to the finite state model. Besides the complexity problem, which can make this approach impractical to implement, when checking LTL properties, different linearizations of the same MSC execution may not agree on the satisfaction of a given LTL specification.

[0006] Another known verification method for HMSCs is based directly on the partial order semantics of HMSCs. Verification according to this method requires specifying properties of HMSCs using HMSCs. Intersecting two HMSCs is analogous to checking the intersection of a system automaton and a specification automaton in the automata-theorectic approach to model checking. Automata-theoretic model checking is discussed in M. Y. Vardi, P. Wolper, “An Automata-theoretic Approach To Program Verification,” Proc.1st Annual Symposium on Logic in Computer ScienceIEEE, 1986. In this method, the specification automaton specifies the disallowed executions. This is done to avoid the process of complementation. Unfortunately, the problem of checking HMSC intersections in this method is also undecidable.

[0007] Model checking of HMSCs is also discussed in A. Muscholl, D. Peled, Z. Su, “Deciding Properties for Message Sequence Charts,” FoSSaCS, Foundations of Software Science and Computation Structures, Lisbon, Portugal, LNCS 1378, 226-423. In the approach to HMSC model checking described therein, the HMSC specifying disallowed executions is given a relaxed interpretation: the HMSC specifies the essential ordering between some events; however, it allows more events and additional ordering to be included in each execution. In essence, this framework amounts to pattern matching between two HMSCs.

[0008] In the method according to the principles of the invention, a temporal logic is used to check a property of a system modeled with a causal (partial order) structure, such as a hierarchical message sequence chart (HMSC). The logic is interpreted over the causal structures. One such logic is a subset of “temporal logic causality” (TLC) and is used to define a specification for the property of interest. This subset of TLC (hereafter “TLC⁻”) provides a logic for expressing specifications that can be automatically translated into a specification automaton. In the method according to the principles of the invention, an implementation automaton is constructed from the causal structure. Property checking then proceeds by checking an intersection of the specification automaton and the implementation automaton for emptiness.

[0009] The property checking method according to the principles of the invention can be implemented in a general purpose computer. A memory stores TLC⁻ specifications, HMSCs, and instructions which, when executed by the computer processor, causes the processor to carry out the method of the invention. In one aspect, the temporal logic specifications are expressed in PROMELA (PROcess MEta LAnguage) code, which is the input language for the SPIN model checking system. When expressed as PROMELA code, the SPIN system causes the computer to use the specification in the model checking method according to the principles of the invention.

[0010] A more complete understanding of the invention may be obtained from consideration of the following description in conjunction with the drawings in which:

[0011] FIG. 1 shows an exemplary message sequence chart (MSC);

[0012] FIG. 2 is the partial order representation of the MSC of FIG. 1;

[0013] FIG. 3 shows an exemplary high-level message sequence chart graph;

[0014] FIG. 4 shows an implementation automaton according to the principles of the invention;

[0015] FIG. 5 is a flow chart depicting a high level description of the method of the invention; and

[0016] FIG. 6 shows an exemplary apparatus for carrying out the method of the invention.

[0017] Model checking of hierarchical message sequence charts (HMSCs) using temporal logic causality specifications is described herein. Referring to FIG. 5, a high-level flow diagram 500 is shown to illustrate the method according to the principles of the invention. The described method derives in part from properties of HMSC expressions and from the automata-theoretic approach to model-checking. In a process step 502, a HMSC is received for property checking. A subset of temporal logic causality is defined, as at 504, for expressing specifications that can be automatically translated to a specification automaton, as at 506 and 508. An implementation automaton is constructed from the HMSC, as at 510, and the intersection of the specification automaton and implementation automaton is checked for emptiness, as at 512. The following description sets forth the methods and data structures, including formal expressions therefor, used in the property checking method illustrated in FIG. 5.

[0018] A. Message Sequence Charts

[0019] A message sequence chart (MSC) describes a scenario where processes communicate with each other. A scenario includes a description of the messages sent, the messages received and local events, as well as the ordering between them. Graphically, a vertical line represents each process, while a horizontal or slanted line represents a message from the sending process to the receiving process. FIG. 1 shows an exemplary MSC. The MSC includes three processes, P1, P2 and P3, described graphically as boxes (102, 104 and 106, respectively) and process lines (108, 110 and 112) from top to bottom. The three processes exchange six messages, M1 to M6, shown as arrows (114, 116, 118, 120, 122, 124 and 126). The arrows show the direction of the message. When a process sends a message a send event occurs, and when a process receives a message a receive event occurs.

[0020] For purposes of this description, an MSC can be assigned a semantic interpretation as a partially ordered set of events. An MSC M is a sixtuple <V <, L, T, m, P> where V is a set of events, <◖ V x V, P is a set of processes, L : V→P is a mapping that associates each event with a process, and T:V→{s, r, l} is a mapping that describes the type of each event (send, receive or local). m◖V x V defines a relation between send and receive events. For any MSC, if (e,f)εm then T(e)=s and T(f)=r. In this case, e and f are a matching pair.

[0021] The order relation < is called the visual ordering of events, and it is obtained from a syntactical representation of the chart (for example, represented according to the standard syntax ITU-Z.120). Assuming first in-first-out message passing for two events e and f, e<f if one of the following holds:

[0022] e and f are the send and receive events of the same message (e and f are called a message pair); or

[0023] e and f belong to the same process P, with e appearing before f on the process line (this imposes a total order among all events of P, for every process PεP).

[0024] For this formal definition, e→f describes the situation where e<f and either e and f are the send and receive of the same message, or there is no event between e and f on some process line (e immediately precedes f). Stated formally, immediately precedes means, if v→W, then there is no u such that v<u<w.

[0025] The partial order between the send and receive events of FIG. 1 is shown in the graph 200 of FIG. 2. Only the “immediately precedes” order is shown in the graph 200. The MSC in FIG. 1 describes an interaction between three processes, P1, P2 and P3. In the illustrated partial order of FIG. 2, process P1 sends the message M1 to P2. After receiving that message, process P2 sends two messages, M2 and M3, to P3. After receiving M3, process P3 sends the message M4 back to P2 and later also sends the message M6 to P1. Process P2, after receiving M4, sends M5 to P1. The message M5 is received by process P1 before the message M6. The send events of the two messages, M5 and M6, are unordered.

[0026] Multiple MSCs over the same set of processes can be joined, or concatenated, to form a single extended MSC. Concatenation permits description of MSC scenarios from an HMSC. For example, the concatenation of the MSCs referenced by the nodes in a path through the graph can describe a single scenario in the system. The concatenation of two MSCs can be expressed from the definition of an MSC. Given MSCs M₁=<V₁, <_{1, L1}, T₁, m₁, P> and M₂=<V₂, <₂, L₂, T₂, m₂, P> over the same set of processes P, and given disjoint sets of events V₁∩V₂=Ø, the concatenation, M₁M₂, is <V₁∪V₂, <, L₁∪L₂, T₁∪T₂,m₁∪m₂, P>, where <=<₁∪<₂∪{(p, q)|L(p)=L(q)pεV₁q εV₂}. According to this expression, the events of M₁precede the events of M₂for each process, respectively.

[0027] Since a complex system like a communications system includes many different scenarios, the multiple MSCs describing the system are joined in a high level description (HMSC). This description consists of a graph having nodes and edges, where each node contains one MSC. An exemplary graph 300 according to the principles of the invention is shown in FIG. 3. The graph includes four nodes (302, 304, 306 and 308). Each node references an MSC. Arrows, also called edges, (310, 312, 314 and 316) connect the nodes. The illustrated system includes three processes, p1, p2 and p3. In the designated initial state 302, p1 sends a CONNECT message to p2, where it is received. p2 can send one of two messages to p1: APPROVE or FAIL. In the scenario where p2 sends an APPROVE message to p1, no other events take place. Where p2 sends a FAIL message to p1, one of two scenarios can take place. In one scenario, p2 also sends a REPORT message to p3. Control returns to p1, which sends a REQ_SERVICE message to p3. In the other scenario, the system returns to the initial state and p1 sends a CONNECT message to p2. Such scenarios can be used to denote the communication structure of typical or exceptional executions of a system, or a counterexample found during testing or model checking.

[0028] In this description, an HMSC N, such as the HMSC 300 of FIG. 3, is a triple (M, τ, M_o), where M is a set of MSCs, all with the same set of processes, and with sets of events disjoint from one another. τ⊂M×M is the edge relation and the initial MSC is M_oεM. An execution of N is a path §=M_oM₁M₂M₃. . . of N that starts with the initial MSC M_oand either ends with a state without outgoing edges, or is infinite. To define an extended MSC for a given scenario, the simple MSCs referenced by the nodes in the scenario are concatenated according to the principles of the invention.

[0029] B. The Logic TLC

[0030] The temporal logic TLC⁻ defined here is a subset of the logic TLC described in R. Alur, D. Peled, W. Penczek, “Model-Checking of Causality Properties,” LICS'95, 10th Symposium on Logic in Computer Science, IEEE, 1995, 90-100. The logic TLC, and its subset TLC⁻, are interpreted over the partial order structure of the HMSCs, and, therefore, do not distinguish between the different linearizations of each partial order execution. Since TLC⁻ can be interpreted over linearizations of the partial order, a single linearization suffices for each execution. This amounts to partial order reduction.

[0031] Expressed formally, a model of the logic TLC⁻ is a partial order ζ=(V, <,→), where <⊂V×V is a partial order relation, and →⊂< is the “immediately precedes” relation. In this embodiment, the set of formulas of TLC⁻ over a set of atomic propositions AP is set forth below:

[0032] true, false ε

[0033] If pεAP, then pε

[0034] If φ, ψ are in then φ,ψ, φψ, φ, ∃οφ, φUψ,φRψε

[0035] An interpretation function I: V2^APassigns to each event of V a set of propositions from AP. Each proposition in AP represents some property (e.g., the event, or the local state before or after the event). I(ν) returns the set of atomic propositions that hold for ν.

[0036] In the logic according to the principles of the invention, the semantics are defined as follows:

[0037] (ζ, υ) true.

[0038] (ζ, υ)p if pεI(ν)

[0039] (ζ, υ)ψψ if(ζνφ and (ζ, φ.

[0040] (ζ, υ)φ if it is not the case that (ζ, υ)φ.

[0041] (ζ, υ)∃οφ if for some w such that ν→w, it holds

[0042] that (ζ, w)φ.

[0043] (ζ, υ)φUψ if there is path ν=ν₀→ν_i→ . . . →ν_n,

[0044] such that (ζ, ν_n)ψ, and for 0<i<n,(ζ, υ_i)φ.

[0045] Some modalities in the logic are defined in terms of modalities that were given a semantic interpretation, although the modalities have no semantic interpretation of their own:

[0046] false=true,

[0047] φv ψ≡(φψ)

[0048] φRψ≡(φU ψ)

[0049] ∀οφ≡∃οφ.

[0050] As is known, TLC contains a universal until operator U and an existential release operator R. For TLC⁻, the until operator, U, is existential and its dual release, R, is universal. The modalities U and R satisfy the following equations:

[0051] φUψ≡ψv (φ∃οφUψ)

[0052] φRψ≡ψ(φv ∀οφRψ)

[0053] Two additional modalities, ⋄ and □, are defined in terms of the above:

[0054] ⋄φ≡trueUφ, and

[0055] □φ≡falseRφ.

[0056] In the method of the invention, the above TLC⁻ logic is used to write specifications for checking HMSCs. An HMSC satisfies a TLC⁻ specification when each execution satisfies the specification. Some exemplary specifications can be written as follows:

[0057] □(req→⋄ack) Every request is causally followed by an acknowledgment.

[0058] □(recA→∃οsendB) Immediately after receiving a message A, a message B is sent.

[0059] ⋄(tranA⋄(tranB⋄tranA)) Transaction B cannot interfere with the events of transaction A.

[0060] □(beginA→∃ο(tranAU finishA)) The execution of transaction A is not interrupted by any other event. As should be apparent, other specifications can be written in the TLC⁻ logic described above.

[0061] In the method of the invention, the TLC⁻ formulas or specifications are interpreted over MSC linearizations. Each linearization is the completion of an MSC execution into a total order. All the linearizations of a single MSC execution must agree with their origin MSC upon the interpretation of each TLC⁻ formula. Similar to partial order reduction methods, it is sufficient to analyze a subset of the executions that are generated due to the different interleavings of the events. For HMSCs, it is sufficient to analyze one linearization per MSC. Interpreting TLC⁻ formulas over linearizations of MSCs simplifies model checking, and permits the reuse of code that was written for verifying concurrent protocols.

[0062] For the linearization of the execution shown in FIG. 1, each event is denoted as a pair, which includes the type of event (send or receive) and the corresponding process:

[0063] (s, P₁) (r, P₂) (s, P₂) (r, P₃) (s, P₃) (r, P₂)

[0064] (s, P₃) (r, P₂) (s, P₂) (r, P₁) (s, P₃) (r, P₁)

[0065] For the above linearization, the immediate successor of an event in a linearization is not necessarily also a successor under the original partial order. For example, the second (r, P₂) event is immediately followed in the linearization by (s, P₃) but not in the partial order. Thus, if ν→w, then ν will appear before (but not necessarily immediately before) w on any linearization. The interpretation of a TLC⁻ formula φ over a linearization ξ of a partial order ζ=(V, <, →) follows the interpretation of φ in ζ. That is, (ζ, i)φ if for the ith event ν of ζ, (ζ, ν)φ (according to the above partial order semantics).

[0066] In the method according to the principles of the invention, TLC⁻ formulas are translated into automata. To facilitate the translation of TLC⁻ formulas into automata over sequences, the syntax of TLC⁻ is extended with three additional types of formulas:

[0067] <P>φ, where P is a process, and φ is a TLC⁻ formula. (ζ, i)<P> φ holds when (ζ,j)φ for some j ≧i, and for each k such that j>k≧i, the kth event does not belong to process P. The formula <P>φ means “the next P event satisfies φ.”

[0068] {MATCH}φ, where φ is a TLC⁻ formula. (ζ,i){MATCH}φ holds when (ζ, j) for some j>i, where the jth event of ζ is the matching receive for the ith event, which is a send.

[0069] NEVER P, where P is a process. (ζ,j) NEVER P holds when for each j≧i, the jth event of ζ does not belong to P. Thus, NEVER P means that no event of P appears later in the linearization.

[0070] For each property φ there is some initiating process Q (a process having the first event from which φ is interpreted). The first event of Q is not a receive event.

[0071] C. Automata-theoretic Model Checking of MSCs

[0072] In the automata-theoretic approach to model checking, a generalized Büichi automaton is a quintuple (S, S₀, Σ, δ, F), where S is a finite set of states, S₀⊂S are the initial states, Σ is the finite alphabet, δ⊂S×Σ×S is the transition relation, and F⊂2^sare the accepting sets. A run ζ over a word a₁a₂. . . εΣ¹⁰⁷ is an infinite sequence of states s₁s₂s₃. . . , with s₀εΣS₀, such that for each i>0, (s_i, a_i, s_i+1)εδ. A run is accepting if one state of F occurs in ξ infinitely many times. A word is accepted by a generalized Büichi automaton when there exists a run accepting it. The language La(A) of a Büichi automaton A is the set of words that it accepts. More genarally, the language of an automaton X is expressed La(X).

[0073] A specification automaton A=(S^A, S₀^A, Σ, δ^AF^A) is a generalized Büichi automaton that represents the disallowed executions. Thus, if η is some temporal specification of an HMSC system, then the corresponding specification automaton accepts exactly the sequences that do not satisfy η. An implementation automaton B=(S^B, S₀^B, Σ, δ^B, S^B) is a restricted version of a generalized Büichi automaton. It has only one accepting set, which includes all the states S^B. Thus, the accepting runs of B are the infinite paths that start from an initial state in S₀^B. An implementation automaton represents the modeled system. The degenerated version of the generalized Büichi acceptance condition is replaced with the more general version when fairness conditions are added to the description of the system.

[0074] The intersection (or product) of an implementation automaton and a specification automaton, expressed as B×A, is (S^B×S^A, S₀^B×S₀^A, Σ, δ′, S^B×F′), where

[0075] δ′={(s, s′), a, (t, t′))|(s, a, t)εδ^BΛ(s′, a, t′)Σδ^A}.

[0076] F′={S^B×𝑓|𝑓ΣF^A}

[0077] Thus, the intersection contains states that are pairs of states of the individual automata. The transition relation relates such pairs following the two transition relations. The accepting states are pairs whose second component is an accepting state of A. The intersection is the language of the product of B and A:

[0078] La(B×A)=La(B)∩La(A).

[0079] The intersection of a specification automaton and an implementation automaton gives all the executions of the implementation that are not allowed by the specification. The intersection is empty if the implementation does not satisfy the specification. Furthermore, any sequence in the intersection can be used as a counterexample. Checking the emptiness of a generalized Büichi automaton can be done by applying the depth first search algorithm to find reachable maximal strongly connected components of the automaton graph. If there exists such a component that includes at least one state from each accepting subset 𝑓εF′, then the automaton is not empty.

[0080] D. Model Checking of HMSCs Using TLC⁻

[0081] Model checking HMSCs according to the principles of the invention uses TLC⁻ as a specific instance of a specification formalism. TLC⁻ allows an efficient translation from TLC⁻ into automata. An on-the-fly LTL translation method is discussed in R. Gerth, D. Peled, M. Y. Vardi, P. Wolper, “Simple on-the-fly automatic verification of linear temporal logic,” Protocol Specification Testing and Verification, 3-18, Warsaw, Poland, 1995, Chapman & Hall. In the method of the invention, a TLC⁻ formula η, is translated into a corresponding Büichi automaton A, which accepts the linearizations that satisfy η. This is a Büichi automaton over linearizations of MSC executions, represented by sequences of events that contain forward edges. The forward edges introduce another constraint on acceptance. The model checking method is appropriate for systems with first-in-first-out, asynchronous message passing. There is no fixed dependence relation between the different events according to the process to which they belong.

[0082] 1. Constructing the Specification Automaton A

[0083] In an exemplary method according to the principles of the invention, TLC⁻ formulas and subformulas are represented in negation normal form to facilitate translation to a specification automaton. In this form, the negation operator is applied to atomic propositions. Each TLC⁻ formula can be converted into an equivalent formula in normal form by repeated use of the DeMorgan laws and the dualities between U and R previously presented. For example, this method yields the following transformations:

[0084] ∃ο(pR(qvr))≡∀ο∃(pR(qvr))≡∀ο

[0085] (pU(qvr))≡∀ο(pU(qr))

[0086] Due to the existence of forward edges in the linearizations, the automata have two transition relations. Each automaton has the form (S, S₀, Σ, L, δ, C, F), where the additional component C is a relation between pairs of nodes. Thus, the intersection of a specification automaton (S^A, S₀^A, Σ^A, L^A, δ^A, C^A, F^A) with an implementation automaton (S^B, S₀^B, Σ^B, L^B, δ^B, C^B, F^B) has an additional component C′, which is C^A∩C^B∩(S′×S′).

[0087] In the construction of the specification automaton, each node in S contains a safety component and a liveness component. The safety component is responsible for guaranteeing the consistency between each node and its successors. The safety component contains certain structures:

[0088] One of the event-type propositions: send, receive or local, for the type of the current event. In addition, it may include the proposition start.

[0089] A maximal noncontradicting subset of the subformulas of the checked property and their negations (in negation normal form). That is, for each subformula φ, each node will contain either φ or φ, but not both.

[0090] If the node does not contain NEVER P, then it contains a maximal noncontradicting subset of the formulas of the form <P>φ, where P is a process and φ is a subformula of the checked property. If a node contains NEVER P, it cannot contain formulas of this type.

[0091] If the node is a send event, then it contains a maximal noncontradicting subset of the formulas of the form {MATCH}φ where φ is a subformula of the checked property. Otherwise, it cannot contain formulas of that type.

[0092] Exactly one process predicate P, for one of the processes of the checked HMSC, except for the first node, which contains all the process predicates.

[0093] If a node contains the process predicate P, then for each formula of type <P>φ that it contains, it also contains φ.

[0094] The liveness component together with an appropriate acceptance condition guarantee that in every accepted run of the automaton, for all the nodes where a subformula of the form φUφ holds, ψ will hold in the current or in a subsequent node. The liveness component contains a subset of the formulas of the form φU φ and <P>φU ψ described above.

[0095] The set of directed edges between pairs of nodes satisfy certain constraints. The constraints are described according to the type of subformulas that appears in the safety component of a given node. They apply to each node that contains such a formula and to its immediate successor according to the relation δ^A. When an enumerated list of constraints is given for a certain type of subformula, then at least one of them applies. In the following list, the condition on the safety component appears in roman fonts, while the condition on the liveness component is given in italics. The process predicate in the current node is given by Q.

[0096] ∃οφ

[0097] 1. <Q>φ holds for each successor, or

[0098] 2. the current node has both the proposition send, and {MATCH}φ.

[0099] ∀οφ

[0100] 1. The current node has receive or local. Each successor has <Q>φ, or

[0101] 2. the current node has send and {MATCH}φ. Each successor has <Q>φ, or

[0102] 3.The current node has send and {MATCH}φ. Each successor has NEVER Q.

[0103] φU ψ

[0104] 1. The current node has ψ, or

[0105] 2. the current node has φ, send and {MATCH}φUψ,or

[0106] 3 . the current node has φ. Each successor has <Q>φUψ. If the liveness component of the current node contains φUψ, then the liveness component of each successor must have <Q>φUψ.

[0107] φRψ

[0108] 1. The current node has both φ and ψ, or

[0109] 2. the current node has ψ, send and {MATCH}φRψ, each successor has <Q>φRψ, or

[0110] 3. the current node has ψ, send and {MATCH}φRψ, each successor has NEVER Q, or

[0111] 4. the current node had ψ and either receive or local. Each successor has <Q>φRψ.

[0112] φvψ

[0113] 1. The current node has φ, or

[0114] 2. the current node has ψ.

[0115] φψ

[0116] The current node has φ and ψ.

[0117] <P>φ

[0118] 1. The current node has Q=P, and φ. If φ is of the form δUψ and liveness component has <P>δUψ, then the liveness component of the current node must also have δUψ, or

[0119] 2. the current node has Q≠P. Each successor has <P>φ, If φ is of the form δUψ and the liveness component has <P>δUψ. Then the liveness component of each successor node must have <P>δUψ.

[0120] NEVER P

[0121] The current node has Q≠P. Each successor has NEVER P.

[0122] start

[0123] If the liveness component of the current node is empty, then the liveness component of each successor consists of the formulas of the type φUψ and <P>φUψ that are included in the safety component of the successor.

[0124] The last case satisfies the situation where all the previous liveness constraints were satisfied, and new ones are loaded from the safety component. Synchronizing with nodes that start a linearization of an MSC, marked with the proposition start, guarantees that there are no forward edges that propagate liveness constraints ‘over’ the current node.

[0125] The construction of the specification automaton also makes use of forward compatibility between states. Forward compatibility means that a forward edge is permitted between the nodes, rather than enforced. A state s is forward compatible with a state t if four conditions hold:

[0126] 1. s has a send proposition.

[0127] 2. t has a receive proposition.

[0128] 3. For each formula of type {MATCH}φ s, the formula φ is in t.

[0129] 4. If the safety component of s contains a formula of the form {MATCH}δUψ, then the liveness component of t must contain δUψ.

[0130] The nodes of S^Aof the constructed specification automaton are defined by splitting the nodes defined above as follows: for a forward compatible pair of nodes s and t, s is split into s₁and s₂, such that both copies have the same incoming edges as the original s. C^A(s,t) is set and the relation C′ is redefined:

[0131] {((s, s′), (t, t′))|(s, s′)εS′ (t, t′)εS′ (s, t)εC^B→(s′,t′)εC^A}

[0132] The asymmetric definition is due to the fact that the set S^Ais a compact representation of the actual states of the automaton A, as described above.

[0133] It is also assured that formulas that need to be satisfied further down the linearization will eventually be satisfied, rather than postponed forever. This is done using the Büichi acceptance set: it contains all the states that include the empty liveness component. This guarantees that all the constraints that were loaded at the previous node with start are satisfied. New constraints are loaded at the next node. Unlike the LTL construction, the liveness constraints can change, e.g., from <P>ηUμ into ηUμ.

[0134] 2. Constructing the Implementation Automaton B

[0135] The implementation automaton B recognizes a single linearization for each execution of a given HMSC N=(M, τ, M_O,). For any MSC M εM, to construct an automaton B_Mthat recognizes a single linearization of M, the ith node along the single execution of this automaton is labeled with the propositions of the ith event in the linearization. The linearization can be done using a topological sort in linear time in the number of events of M. The first node in each such linearization is marked with start.

[0136] In one exemplary construction, denote by first (B_M) the initial state of B_Mand by last (B_M) the final state. Let M¹,M², . . . , M^kbe the successors of M under the relation τ, MτMⁱfor 1≦i≦k. To that, add the set of transitions (last(B_M), α, init (B_M)) for 1≦i≦k. After executing B_M, there is a nondeterministic choice to any off the initial states of the automata representing the successor MSCs of M. Label these edges with the proposition start. The implementation automaton is then linear in the size of the checked HMSC.

[0137] An automaton for the HMSC 300 of FIG. 3 constructed according to the principles of the invention is shown in FIG. 4. The automaton 400 includes four states (402, 404, 406 and 408). Each state includes various nodes corresponding to the send and receive events in the linearization. Forward edges are shown as dotted arrows (408, 410, 412, 414 and 416). Nodes that are marked with an asterisk ‘*’ are labeled with the proposition start.

[0138] 3. Checking the Intersection of the Automata

[0139] Checking the intersection of the specification and implementation automata implements a decision procedure similar to the one for traditional Büichi automata. To avoid undecidability arising from two successor relations, the following restrictions apply:

[0140] One of the relations (the forward edges) is embedded in the transitive closure of the other relation (representing the linearization successors).

[0141] There is a finite bound on the number of successor edges between the source and the target of each forward edge. This is due to the fact that communication is limited to occur within a single HMSC node.

[0142] There are no forward edges (i.e., the second relation) that ‘overtake’ the accepting states, i.e., starting before an accepting node and ending after it.

[0143] Due to the forward edges, the intersection of these two automata has an additional constraint. During a depth first search (DFS) performed to check the emptiness of the intersection, when a receive node is reached, the DFS traces back to the corresponding send. The send already should be on the DFS stack. The implementation automaton B fixes the distance of the send event corresponding to the current receive event. In the intersection DFS stack, the send node will be down the stack the same distance from the receive node as it is in B. The components of the automaton A on the DFS stack are checked for forward compatibility. If there is no compatibility, the DFS backtracks. Due to the above mentioned constraints on the forward edge relations, checking for emptiness of the intersection is done by searching for a reachable cycle through an accepting state of the intersection.

[0144] E. Computer Based Implementations

[0145] FIG. 6 illustrates an exemplary embodiment of a computer-based system 02 for carrying out the method of the invention. The system 02 comprises a processing unit 07, a display screen terminal 08, input devices, e.g., a keyboard 10, and storage devices, such as a hard disk 09. The processing unit 07 includes a processor 04 and a memory 06. The memory 06 includes areas for storing, among other things, instructions for the processor 04. A selection device 12 is operable to select objects displayed on the display 08 when the system 02 operates with a graphical user interface (GUI). The screen 08, keyboard 10 and selection device 12 are collectively known as user interface devices. The system 02 utilizes a computer operating system and a windowing system for providing an interface between the user and the GUI. The operating system and the windowing system can be found resident in the memory 06.

[0146] Processor 04 is a general-purpose processor capable of executing a stored program routine that implements the verification method described herein. Memory 06 can consist of a single memory chip or multiple banks of memory, and the memory 06 can include Read Only Memory (ROM) and Random Access Memory (RAM). The storage device 09 is capable of storing and transmitting data and can consist of multiple storage units that are linked together. The storage device 09 may store, among other things, HMSC representations, automata representations, TLC⁻ specifications and the output results produced by the method of the invention. The representations contain the information necessary for the system 02 to display, for instance, an automaton image on the system's 02 display terminal 08. These representations can also be kept in memory 06 and moved to storage 09. Representations and output results stored in the storage unit 09 are transmitted to processor unit 04 through an I/O bus (not shown).

[0147] The HMSC model checking method according to the principles of the invention can be implemented in the above apparatus 02 utilizing the SPIN model checking system which is described in G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall Software Series, 1992. The HMSC is translated from an HMSC notation where each individual MSC is described using the ITU Z.120 standard. Code used for HMSC pattern matching, described in A. Muscholl, D. Peled, Z. Su, “Deciding Properties for Message Sequence Charts,” FoSSaCS, Foundations of Software Science and Computation Structures, Lisbon, Portugal, LNCS 1378, 226-423, can be used for implementing the translation of the HMSCs and the linearizations. The translation results in PROMELA code, which is the input language for the SPIN model checking system. For simplicity, the implementation assumes that no MSC in the HMSC graph is empty. Finite paths are completed to infinite ones with a repeated occurrence of an event that does not belong to any process, and where all the propositional variables are set to false.

[0148] After translating an HMSC and a TLC⁻ formula into PROMELA code, the SPIN model checking tool can be used to make the automatic verification. If the HMSC does not satisfy the specification, a counter example is found. Simulating the counterexample using SPIN outputs a sequence of the HMSC's nodes that participate in the counterexample. Then, the POGA tool can display the MSC execution on the display 08. The POGA tool is described in G. J. Holzmann, “Early Fault Detection Tools,” TACAS 1996 Tools and Algorithms for Construction and Analysis of Systems, LNCS1055, Springer, 1-13.

[0149] As detailed above, the invention can be embodied in the form of methods and apparatuses for practicing those methods. The invention can also be embodied in the form of program code embodied in tangible media, such as floppy diskettes, CD-ROMs, hard drives, or any other machine-readable storage medium, wherein, when the program code is loaded into and executed by a machine, such as a computer, the machine becomes an apparatus for practicing the invention. The invention can also be embodied in the form of program code, for example, in a storage medium, loaded into and/or executed by a machine, or transmitted over some transmission medium, such as over electrical wiring or cabling, through fiber optics, or via electromagnetic radiation, wherein, when the program code is loaded into and executed by a machine, such as a computer, the machine becomes an apparatus for practicing the invention. When implemented on a general-purpose processor, the program code segments combine with the processor to provide a unique device that operates analogously to specific logic circuits.