With the rapid development of information technology, the real-time system is becoming more and more wildly used. In order to design a real-time system correctly, the legitimate model of the real-time system should be given in early stage of system analysis. The Unified Modeling Language UML has been used to build models for such complicated systems. The UML model can be divided into static structure model, as well as dynamic behavior model. The static structure model concentrates on the structural information of the system, while the dynamic behavior model pays more attentions to the behavioral information of the system. Generally, the dynamic behavior model is more complicated and important. The method to build the dynamic behavior models for the real-time system using UML is one of the research aspects in this paper.At the same time, the real-time behaviors of the systems can be described by time constraints. However, UML is a kind of graphical language, whose semantics can be described by natural language, and have some ambiguities. Therefore, it is a urgent demand for UML to have the formal semantics. It is also the focus of this paper to integrate the UML and formal language, make up the shortfall of UML semantics, and give precise semantic of real-time behavior model.The main contributions of this paper include:Researched Interaction overview diagrams, which are newly imported in UML2, proposed a kind of method that can build the models for real-time system based on Interaction overview diagrams, and illustrated this kind of method through real example. Compared with the traditional one, this method is more straightforward and comprehensive, and can control the dynamic behaviors of the systems as a whole.Gave the formal definition of the relationship between UML Sequence diagrams and time constraints, which include the simple Sequence diagrams, Sequence diagrams with Combined Fragment and consistency of time constraints, based on the former research. Extended the time attributes of the Sequence diagrams, in order to describe the real-time system. The precise formal description is the basement of the research, and all the analysis and verification behind are based on it.Proved the theorem of Sequence diagrams with Combined Fragment accord with time constraints, and proposed a verification algorithm, which can be used to verify whether the UML Sequence diagrams having time attributes complied with some time constraints, based on this theorem. The Sequence diagrams having time attributes make the modeling of real-time system more convenient. The Security of the real-time system has been promoted by verifying whether the behaviors of system confined to time constraints. |