Consistency Verification Of Dynamic Behavioral Models In Real-time Software Based On UML2.0

Nowadays, real-time systems have been widely used in national defense, aeronautics and astronautics, communications, etc. With the real-time systems growing up in their scale and complexity, In order to comprehend the system better and develop a high quality real-time software,It is necessary to construct the models of the software.UML is the de facto standard for the modeling of large scale and complex software system,and also widely used in the area of real-time software development.when using UML to develop the real-time software a problem that frequently encountered is the inconsistency between different models of UML.It is necessary to detect the inconsistency and correct it in the early stage of the software development.Based on the background stated above, the consistency verification between UML2.0 sequence diagram models and State Machines models in the real-time software has been studied in this paper. The consistency is divided into syntactic consistency and semantic consistency.The correctness of computations in real-time system not only depends on the logic correctness of the computation but also depends on the time at which the result is produced, if the time constraints of the system are not met , system failure is said to have occurred, so in semantic consistency we studied behavioral consistency and time consistency. The specific studies are as follows:(1)Present the precise definition of UML sequence diagrams and state diagram in the form of syntactic and semantic,further analysis and verification is based on this formal description.(2)Study the relationship between the events in the sequence diagram, after that an automata is introduced to depict the events that every object participated in the scenario, then the automata is extended to describe the UML2.0 sequence diagram that contains combined fragment.The time modeling mechanism in UML2.0 sequence diagram is analyzed, after that an algorithm is introduced to extract the timing constraits from UML2.0 sequence diagram. (3)Add time constraits to UML2.0 State Machime to model real-time systems, then introduce a method that use UML2.0 State Machine network to model the dynamic behavior of real-time software.Research the transformation from State Machine network to timed automata network, which facilitate the formal analysis and verification using UPPAAL.(4)Work on the consistency verification between UML2.0 sequence diagrams model and State Machines model in real-time software based on the above work. Finally, the automobile gear control system is taken as an example to show our method of consistency verification.