Font Size: a A A

Research On UML Timing Diagram Model To UPPAAL Timed Automata Model Transformation Method And Its Tool To Achieve

Posted on:2012-12-10Degree:MasterType:Thesis
Country:ChinaCandidate:K L CuiFull Text:PDF
GTID:2178330332467376Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
Any small error in real-time systems may result in disasters.Therefore, ensuring correctness and reliability is a primary factor for establishing real-time systems. Modeling real-time systems is no doubt a good solution, but new problem following is how to ensure the correctness and reliability of the model. This depends on a well-defined modeling language and perfect tools for modeling, simulation and verification.As a standard language for describing software structures and behaviors visibly, UML has been used widely in varieties of software development and plays a more and more important role in real-time areas. At present, UML sequence diagram and state diagram are mainly used in real-time system modeling. However, UML timing diagram can describe not only the state translation but also the order and details of interaction perfectly. Powerful and flexible description ability of timing diagram will make itself more and more significant in real-time system modeling.High reliability in real-time systems requires simulating and verifying the system model. UPPAAL is a tool based on timed automata to verify real-time systems and has powerful simulation and verification capabilities. However, UPPAAL can only verify models described by UPPAAL timed automata, but not UML timing diagram models. If UML timing diagram models can be translated into UPPAAL timed automata models, then UPPAAL can be used to simulate and verify real-time systems based on UML timing diagram.Furthermore, if a tool translating them automatically is developed, then UML timing diagram models can be directly input into UPPAAL instead of rebuilding models in UPPAAL,which consequently shortens the development period and reduces error probability.In this paper, UML timing diagram model and UPPAAL timed automata model are analyzed, and the translation strategy translating UML timing diagram model into UPPAAL timed automata model is presented. According to the semantics of elements in UML timing diagram and related semantics in UPPAAL timed automata, design plan mapping UML timing diagram model to UML timed automata model as well as translation algorithm is given.At the same time,the tool-UML_TDMtoUPPAAL_TAM,based on translation rules and algorithms above, is given. According to the defined rules, the tool can translate the UML timing diagram model into UPPAAL timed automata model which will then be simulated and verified by UPPAAL.The translation from UML timing diagram model to UPPAAL timed automata model makes it possible for UPPAAL to verify real-time systems based on UML timing diagram. The translation tool makes UML timing diagram models can be directly input into UPPAAL instead of rebuilding models in UPPAAL. This consequently shortens the development period, reduces error probability, and thus greatly increases the reliability of real-time systems.
Keywords/Search Tags:UML Timing Diagram, real-time system, Timed Automata, UPPAAL
PDF Full Text Request
Related items