A Method of UML Sequence Diagram Verification Based on a Graph Grammar

With the increasing scale and complexity of software, the description of software structure plays a more and more important role. In order to ensure the quality of the software and improve the reliability of the software, it is a feasible way to combine the relevant parts of the software structure with the formal methods. In this paper, based on an existing context-sensitive temporal graph grammar, the formal method for UML sequence diagrams is proposed. Then, new productions are presented, which could be used to verify and analyze the temporal semantics in UML sequence diagrams. Finally, a case study of ATM withdrawal operation is provided to show how the formal method works.