Abstract:In Unified Modeling Language (UML) superstructure standard, the semantics of sequence diagrams are formal defined by natural language, it is a semi-formal language and it can not make formal analysis and proof to system's interbehavior. Aiming at the problem that UML sequence diagram is not able to formal description, according to the temporal characteristic of UML sequence diagram, this study puts forward an six-tuple formalization method based on adding the interaction operators in UML sequence diagram. Temporal Description Logics (TDLs) are proposed by the temporal extending the Description Logics (DLs), which are the formal specification of the dynamic and temporal semantics. The semantic of TDLs is proposed by temporal operators of TDLs. Taking UML sequence diagram of the C Language executing process as an example, a formal methodology description is given out. Examples verify the feasibility of this method.