Message Ordering Verification
In a valid UML model of a software system, the sequence of messages sent and received by an object in a sequence diagram should be consistent with the sequence of messages sent and received by that same object in a state chart diagram for the corresponding class. For example, if a sequence diagram shows a user picking up a phone, dialing a number and then getting a working phone connection, then the corresponding state chart diagram should show a possible scenario where the same sequence of events can occur. In this work, the process of ensuring that sequence and state chart diagram messages are consistent is called message ordering verification.
To perform message ordering verification, the tool constructs a message graph for each state chart diagram and builds a list of messages sent and received by each object in a sequence diagram. After that the goal is to find an initialized trajectory in the message graph that matches the sequence of messages sent and received by the corresponding object.
A message graph is a graph where each graph node represents a type of action in a state chart diagram. This action can be an entry action, do activity, event trigger, event effect, transition trigger, transition effect, or an exit action. Transitions between nodes in the graph indicate actions that are possible after the action in the current node. The message graph therefore is a graph of all possible sequence of actions in a state chart diagram. The figure below illustrates a message graph. The TransStart node is a pseudo-node that is used as a starting point for all outgoing transitions from a state. Also, there is an empty pseudo-node called StubEntry to replace an Entry node if no entry action exists for a state.
Details regarding the construction of the message graph and its operation can be found in the Master's thesis titled A tool supporting validation of UML models in the documentation section of this web site. Here we will proceed with an example showing how the tool performs message ordering verification.
In this example we have a UML model of the DHCP protocol. The figure below shows the sequence diagram indicating the messages exchanged between the user, the DHCP server, DHCP client, and IP address objects. The two figures after that show examples of state chart diagrams for the DHCP client and server classes respectively.
Sequence diagram for DHCP
State chart diagram for a DHCP client
State chart diagram for a DHCP server
The job of the tool is to find out whether the sequence of messages seen by the DHCP_Client object in the sequence diagram is a possible sequence in the state chart diagram for DHCP_Client and similarly for the DHCP_Server object. For instance, the sequence of messages seen by the client/aClient object is:
- Receive
initiate - Receive
connect - Send
discover - Receive
offer - Send
request - Receive
ack
The tool then tries to find a path within the message graph (or its equivalent, the state chart diagram) that has this sequence of messages. Received messages include triggers and events while sent messages include entry and exit actions, do activities, event effects and transition effects. By manually comparing this sequence of messages with the state chart diagram for the DHCP_Client class one can conclude that this sequence is valid.
State chart diagrams can contain guards on transitions, which are boolean expressions that have to evaluate to true before a transition can be triggered. At this point our tool has no support for automatically evaluating guards so the tool will ask the user to specify the evaluation result when it needs to try a transition while searching for a message sequence match. It is up to the user to decide whether a guard should be true or false. The figure below shows a screenshot of the prompt.
From the preceding figure one can see that the DHCP_Server object had a correct sequence of messages in the sequence diagram. If the tool does not find a path in the message graph matching the sequence of messages, it will display the longest match possible so developers can try to figure out the problem. For instance, if we answered false to the guard in the DHCP_Server state chart diagram the tool cannot find a match and displays the error similar to the one in the figure below.
