Research On Transformation Of UPPAAL Timed Automata To UML Diagram And The Implementation Tool

The safety and reliability of software model in the design phase is of significant importance, especially to the real-time system. Formal method, which is based on strict mathematical theory, is widely used to model, simulate and verify real-time system in order to ensure its reliability. One of the formal verification tools, UPPAAL, which is based on timed automata, can be adopted to model and verify real-time system as timed automata. In fact, timed automata theory has been successfully applied to verify communication protocol and model train control system, such as the GRC problem. However, software designers typically use UML (Unified Modeling Language) to model the system, and then try to verify the validity of this model.In order to verify the UML model in UPPAAL, research on transformation of the UML timing diagram model to UPPAAL timed automata has been conducted. If the reverse transformation can be realized, without doubt the designers could model in UPPAAL, verify it, and then transform it to the UML model. Moreover, once the previous object model—the UPPAAL model turned out to be wrong; it can be fixed and then transformed back to UML.This thesis presents the transformation of UPPAAL timed automata to UML diagram. First, the characteristic and syntax of UPPAAL are given, followed by the introduction of UML timing diagram and class diagram. The reason to choose these two sub-diagrams is that class diagram reflects static structure of the system while timing diagram presents dynamic interacting details, both of which are indispensable in modeling real-time system.Furthermore, we analyzed the syntax of elements in UPPAAL timed automata and UML diagrams respectively; then the transformation rules and algorithm are presented.Finally, we design the implementation tool—UPALToUML based on the above rules and algorithm. The use of this tool is shown with a case—pedestrian-controlled traffic lights. The results suggest that UPALToUML can perform well according to the transformation rules.In conclusion, the work we have done in this paper makes it possible for the designers to model and verify the system in UPPAAL first, and then transform it to UML model, which is most often used in software design. At the same time, when the UPPAAL model in UML—UPPAAL transformation went wrong, it can be directly modified in UPPAAL instead of the UML model. This paper also extends previous UML timing diagram to the combination of timing and class diagrams, achieving the unification of UML dynamic and static diagrams.