Model checking of message flow diagrams

Details Model checking of message flow diagrams Model checking of message flow diagrams

1999-08-17

2003-02-04

Black, Thomas (Department: 2121)

Data processing: artificial intelligence

Plural processing systems

C703S002000, C703S015000

Reexamination Certificate

active

06516306

ABSTRACT:

FIELD OF THE INVENTION
The invention relates generally to model checking in systems design and more particularly to model checking of message flow diagrams.
BACKGROUND
The design of complex software-related systems includes requirements engineering, model analysis, code construction and testing. The requirements engineers typically prepare a requirements document which describes the required or anticipated behavior of the new software in written prose. The requirements state the expected behavior of a system component in response to a particular sequence of external stimuli. The requirements document then serves as the input for constructing models that exhibit desired properties of the system. Software engineers use the models to build the code. The models may also serve as input in designing tests to test the code.
Model checking in systems design verifies that a model satisfies certain desired properties, such as the behavior of a communications switch or other component. If a model contains errors, the errors are transferred to the software engineers during coding and to the test engineers during test design. Any code or test case constructed from the model will likely exhibit the same errors as the model. These errors may not be discovered until acceptance testing, or worse, after the system is fully installed.
It is a disadvantage of traditional system design methods that textual requirements documents cannot be model checked. Since model construction and checking occurs later in the development cycle than the preparation of requirements documents, errors are also not revealed until later in the design of the system. These errors, if discovered during the requirements phase, can be corrected prior to model construction.
Message flow diagrams—also known as time sequence diagrams, message sequence charts (MSCs), or object interaction diagrams—are a popular formalism for documenting design requirements for concurrent systems, such as telecommunications software. MSCs are often used in the first attempts to formalize design requirements for a new system. In one form, MSCs depict the desired exchange of messages between processes in a system for one system execution or scenario. In another form, message sequence chart graphs (MSC-graphs) and hierarchical message sequence charts (HMSCs) can depict multiple scenarios of a given system or system feature. Since MSCs, MSC-graphs and HMSCs are often constructed at an early stage of design, any errors revealed in these formalisms benefits the remaining design effort.
Despite the many advantages in using message flow diagrams to document design requirements, there are few known methods for verifying that MSCs, MSC-graphs or HMSCs exhibit desired system behavior. One method requires translating MSC based specifications to communicating finite state machines and to analyze the resulting state machines to verify behavior. In this method, each process must be modeled as a state machine and then model checking is performed on the composition of the state machine. Analyzing communicating state machines, however, is computationally inefficient and results in a bottleneck during the model-checking phase of system design. Furthermore, the advantages of expressing design requirements as MSCs, MSC-graphs or HMSCs, such as the ability to view the parallel behavior of multiple processes, is compromised when they are converted to multiple state machines. The communicating state machines do not specify the exact same behaviors as the MSCs. The need remains, therefore, for a method system for model checking requirements specification such as MSCs.
SUMMARY
A system and method according to the principles of the invention provides for computationally efficient model checking of message flow diagrams such as message sequence charts (MSCs), MSC-graphs, and hierarchical message sequence charts (HMSCs). This permits behavior verification at an early stage of the development cycle. In an exemplary embodiment, verification is performed on an MSC. The MSC specifies a finite set of events where each event is labeled with a symbol from an alphabet of symbols. All possible linearizations of the partial ordering of events specified by the MSC are mapped over the symbols. These linearizations represent possible interleavings of events in the MSC. The resulting set of mappings, called strings, is referred to as the language of the MSC, and the strings represent the possible executions of the system.
A test automaton is then built to generate or recognize the language of the MSC. To build the test automaton, all the global states of the MSC are extracted. The initial state of the automaton is the state where no events have occurred. The final state of the automaton is the state where all events in the MSC have occurred. The intervening states are extracted by incrementing each process in the MSC by one event at a time over the MSC's possible linearizations. The test automaton then becomes a state machine over the language of the MSC.
To test this automaton, the undesired behavior of the system or system property is defined by a specification automaton that accepts or recognizes the undesirable executions of the system. The specification automaton is a state machine defined by a finite set of states, a set of initial states, an alphabet, a state transition relation, and a set of accepting states. The state transition relation defines the automaton's state transitions. The accepting states are defined as states which terminate a string recognized by the automaton; i.e., a string ending in an accepting state is in the language of the automaton. The states and transitions are labeled over the same alphabet as the MSC. To model check the MSC, the system determines whether there is an execution in the intersection between the language of the test automaton and the language of the specification automaton.
MSC-graphs and HMSCs can also be model checked according to the principles of the invention. An MSC-graph is a directed graph having nodes and edges. Each node references an MSC and the edges connect the nodes. Where a path through the graph passes through multiple nodes, the MSCs can be concatenated to form an extended MSC. In an HMSC, the nodes represent a simple MSC or another MSC-graph or HMSC. To model check an MSC-graph or an HMSC, it is first determined whether the intended meaning of the MSC-graph or HMSC is synchronous or asynchronous. In a synchronous MSC-graph or HMSC, every event in a node's referenced MSC occurs before any event occurs in the MSC referenced by the node's successor. If they are asynchronous, no constraint is placed on the timing of events based upon the referencing node's location in the graph or in the HMSC.
To model check synchronous MSC-graphs and HMSCs, they are converted directly to automata. These automata are checked with respect to the specification automaton. In the asynchronous case, model-checking proceeds on bounded MSC-graphs and HMSCs; therefore, asynchronous MSC-graphs and HMSCs are checked for boundedness prior to constructing the automata. They are considered bounded if no process in any cycle sends messages but does not receive a message, directly or indirectly, from any other process in the cycle. Any path in the graph that can repeat without terminating is a cycle. If an MSC-graph or HMSC is unbounded, some set of processes will be a witness to the unboundedness. These processes will send messages to at least one process outside of the set, but no process will receive messages from outside the set.


REFERENCES:
patent: 5812145 (1998-09-01), Holzmann et al.
patent: 6038538 (2000-03-01), Agrawal et al.
patent: 6185516 (2001-02-01), Hardin et al.
patent: 6259451 (2001-07-01), Tesler
patent: 6449711 (2002-09-01), Week
J. Rekers; A graph based framework for the implementation of visual environments, 1996; IEEE 0-8186-7469-5/96; 148-155.*
Frank Slomka,; Schedulability Analysis of Hetrogeneous Systems for Performance Message Sequence Chart; 1998; IEEE 1092-6100/98; 91-95.*
A. V. Aho et al., The Design an

Affiliated with

Also associated with

Rating

Model checking of message flow diagrams does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Model checking of message flow diagrams, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model checking of message flow diagrams will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3158244