A formal method of software specification and a set of mathematics models were put forward based on UML(unified modeling language) sequence diagram. UML sequence diagrams reflect the interaction and sequence of message among the concurrent objects in the system, and hold the important position in software modeling. A formal description of UML sequence diagram and compound sequence diagram was dealt based on UML criterion. The send character and receive character of the message, as well as message consistency in message-sending and message-receiving were analyzed in detail. UML sequence diagram character was proved by example. A formal description and analysis of UML sequence diagram character was proposed, which provided a prior condition for model transforming and model validation, and provided the foundation for automated software test case on UML sequence diagram. The formal definition of UML sequence diagram was used in the construction of a software comprehension and modeling tool.
Schafer T,Knapp A,Merz S.Model checking UML statemachines and collaborations[J].Electronic Notes in Theoretical Computer Science,2001,55(3):357-369
Vitus S W L,Julian P.Consistency checking of sequence diagrams and statechart diagrams using the π-calculus //Proc of the 5th Int‘l Conf on Integrated Formal Methods(IFM 2005).Berlin: Springer-Verlag,2005,3771:347-365
Rasch H,Wehrheim H,Najm E,et al.Checking consistency in UML diagrams: classes and state machines //Formal Methods for Open Object-Based Distributed Systems (FMOODS-03).Heidelberg:Springer,2003,2884:229-243
Pender Tom.UML����[M].����ͩ,ʷ����,Ҷӳ,����.����:���ӹ�ҵ������,2004 Pender Tom.UML bible[M].Translated by Geng Guotong,Shi Liqi,Ye Zhuoying,et al.Beijing:Publishing House of Electronics Industry,2004(in Chinese)
Eriksson H E,Penker M,Lyons B,et al.UML2 toolkit[M].Indianapolis: Wiley Publishing,2004