UML(Unified Modeling Language)is a graphical language for software system development that is powerful and easy to express.To facilitate the modeling and analysis of software systems under development,UML defines a variety of diagrams that describe the system to meet different needs.Among them,sequence diagrams are widely used to interact between objects in time order.However,as a semi-formal model,the sequence diagram cannot accurately analyze and verify the system.The formal description of sequence diagrams is a hot issue,especially the research on the decomposition and composition of reasoning sequence diagrams is not perfect.At present,it is difficult to deal with UML2.0 complex combination fragments for the work of formal semantics of sequence diagrams.This paper proposes event-based formal semantics,which effectively solves the formalization problem of com-bined fragments in sequence diagrams.The problem of communication modeling based on mobility is discussed,and a unified modeling approach for unified mobility and communication is proposed.Based on this formal semantics,this paper presents a new sequence diagram decomposition and composition method.In this paper,the method of decomposition and composition is decompose the global sequence dia-gram into a global sub-sequence diagram.Under the new decomposition method global sub-sequence diagrams can be recomposed into the larger global sub-sequence diagram or global sequence diagram using the composition operation called union without necessarily considering mechanisms such as synchronous communication,asynchronous communication,and broadcast communication of messages.This pa-per first formalizes the sequence diagram.then transforms the sequence diagram into a dependency structure,and then discuss the unified mobility and communication modeling method.finally proposes the decomposition and composition theory of the sequence diagram based on the dependency structure.A case study demonstrates the decomposition method with the support of the tool. |