Research And Implementation Of Real-Time System Modeling And Formal Verification Based On UML And UPPAAL

With the rapid development of computer science and technology,the application of real-time system is more and more widely and its scale is also growing,how to guarantee the reliability of real-time system in the system design stage has became a hot research topic in recent years.In the design phase of real-time system,UML timing diagram model is usually set up for real-time system,this can provide visual guidance for subsequent system development.In order to ensure that the model is correct and meet the reliability requirements of the system,it is necessary to verify the model.Since the UML model is a semi formal model,it lacks precise semantics,so it is difficult to verify directly,as a formal model,timed automata model can be easily verified in some real-time system verification tools.UPPAAL is a formal verification tool based on timed automata theory,it is widely used in the verification of communication protocol analysis,train control system and many other real-time systems,but timed automata model are often difficult to read and understand,so it is difficult to be the visual guidance for subsequent development.In order to facilitate the design and development personnel to use the correct UML sequence diagram for subsequent development,thus to ensure the reliability of real-time system,in this paper,we first analyze the semantics of the model elements in the UML timing diagram and timed automata and research the existing conversion algorithm from UML timing diagram to timed automata,on the basis of it,the problems in practical application are improved,an improved conversion algorithm is proposed to convert the UML timing diagram into timed automata.Secondly,due to the lack of the layout of the timed automata,manual drag is also required to complete the layout,in order to automatically complete the layout of timed automata for verifying timed automata in UPPAAL,based on the existing layout algorithm for directed digraph,this paper proposes an improved layout algorithm for the loop problem in timed automata,and automatically layout the converted timed automata.Finally,after the verification of the timed automata,if errors are found,then correct the timed automata directly in UPPAAL to get the correct timed automata,in order to make developers to use the correct UML timing diagram as a visual guide for subsequent development,based on the semantic analysis of the model elements of UML timing diagram and timed automata,this paper proposes a conversion algorithm from timed automata to UML timing diagram,and uses this algorithm to convert the correct timed automata into UML timing diagram.Based on the above conversion algorithms and layout algorithm,this paper designs and realizes the model transformation and layout tool called MT&L for real-time system,and describes the tool combined with a typical example of real-time system.Through the application in concrete example of the method proposed in this paper,it can be seen that this method meets the high reliability requirements of real-time system,and at same time simplifies the work of system design and development personnel,improves the development efficiency of system.