Semantic Analysis of UML2.0 Sequence Diagram Based on Model Transformation

The Sequence Diagram(SD) of UML2.0 enriches those of previous versions by two new operators, assert and negate, for specifying required and forbidden behaviors. The semantics of SD, however, being based on pairs of valid and invalid sets of traces, is inadequate, and prevents the new operators from being used effectively. The semantic confusions between assert and negate operators in UML SD are significant, since they pose great difficulty to the confirmation of the security of the system they designed. A new Petri-net model named LPNforSD is designed in this paper. Transformation rules from SD to LPNforSD are given out. We take fragment that described by assert or negate operator as independent part and transform it into LPNforSDs. An algorithm is also designed to check whether the SD is safe by comparing its traces with the traces getting from negate and assert fragments. By this way, we cannot only eliminate the semantic confusions between assert and negate operators, but also reduce the numbers of contingent traces. Thus, we can ensure the system more reliable.