| UML (Unified Modeling Language) is a powerful and visualization Object-Oriented modeling language. Different aspects of a system, such as static topology structure, dynamic behavior, and composition mechanism, can be described by different kinds of UML diagrams. Presently UML is widely accepted by software developer to design system model, thus it has become the de factor standard in industry. UML exists in each stage of software life cycle which includes requirement, design, analysis, implement, test, deployment, maintenance and so on.For some security critical system, such as network protocol, traffic control system, embedded real-time parallel system etc., key functional properties and quantitative performance measure should be validated and analyzed at the early stage of requirement and design. However, UML is a semi-formalized meta-model without exact formal semantics, thus key system properties can't be automatically reasoned. If UML is assigned with formal semantics, key system properties can be automatically validated and analyzed by based on model checker.System topology structure is described by static UML diagrams, and system behavior is described by dynamic UML diagrams. In most cases, design and development stuff focus on run-time feature of system. In this paper, dynamic UML diagrams are assigned with formal semantics according to these problems:Firstly, the semantics of UML isn't exact, thus the gap among requirement, design and implement are generated; Secondly, if a system is described by different kinds of UML diagrams, there probably exists confliction in semantics, even for the same kind of UML diagrams in different abstract level, there still possibly exists inconsistency in semantics, too; Thirdly, UML can'model and validate real-time parallel system related to probability, rate and time.Process algebras describe communication parallel system by algebras theory, which are comprised by a group of operators and composition mechanisms of these operators. Process algebras are based on labeled transition system. The core of process algebras lies on the theory of bi-simulation equivalence, which determine whether the behavior of two processes are strong/weak/observational equivalence or not. Firstly, dynamic behavior of UML state diagrams and sequence diagrams can be described by labeled transition system; secondly, the theory of bi-simulation equivalence provides the foundation to validate semantics equivalence among different kinds of UML diagrams.Probabilistic model checking supports discrete-time Markov chains and continuous-time Markov chains, and it is able to model real-time parallel system related to probability, rate and time. Probabilistic model checking is firstly proposed by Birmingham University of United Kingdom and supported by the probabilistic model checker PRISM. PRISM can model and analyzed real-time system related to probability and rate, thus system key quantitative measure can be automatically reasoned and analyzed.In this paper, dynamic UML diagrams are assigned with formal semantics, the main content and innovation of this paper as follows:1. UML state diagrams and sequence diagrams are assigned with LTS operational semantics.UML state/sequence diagrams are comprised of basic constructive elements and several composition mechanisms (or combined fragments). UML state/sequence diagrams are abstracted as a mathematics model, LTS structure are abstracted as another mathematics model. In this paper, the mapping rules from the basic constructive elements of UML state/sequence diagrams to corresponding element in LTS structure are presented; the composition mechanisms (or combined fragments) of UML state/sequence diagrams are assigned with LTS operational semantics and then translated to pi-calculus.UML state/sequence diagrams are firstly assigned with LTS operational semantics rather than directly translated to some process algebras specification, the advantage is as follows:process algebras are based on LTS structure, if it is assigned with LTS operational semantics firstly, arbitrary process algebras specification rather than one specific process algebras specification can be generated according to different syntax paradigm.After UML state/sequence diagrams are translated to specific process algebras, such as pi-calculus, semantics consistency of different kinds of UML diagrams can be validated based on bi-simulation theory by process algebras tools. Dynamic behavior of system can be observed by "step-by-step" execution in process algebras tools to validate whether requirement and design are consistent. 2. Extended UML state diagrams are assigned with probability/stochastic Kripke formal semantics.Extended UML state diagrams have implicit mapping relationship with the syntax and semantics of probabilistic model checking which can model real-time parallel system related to probability and rate. Extended UML state diagrams are abstracted as a mathematics model, probability/stochastic Kripke structure are defined as another mathematics model, and the mapping rules and translation algorithm are proposed to realize the translation between the two mathematics models. Extended UML state diagrams are comprised of basic constructive elements and several composition mechanisms, the advantage are as follows:it is feasible to analyze the correctness of translation algorithm by structural induction.After UML state diagrams are assigned with probabilistic/stochastic Kripke formal semantics, they can model and validate real-time parallel system such as queuing network, Ad Hoc probabilistic network. Quantitative performance measure can be automatically reasoned and analyzed in probabilistic model checker PRISM, and dynamic behavior of real-time system can be observed by "step-by-step" in PRISM.3. The key XMI labels are presented and their data structures are defined, the formal semantics generation algorithm are also presented.In the research work of assigning UML with formal semantics, the mapping rules and algorithms from UML to formal semantics are usually presented in high abstract level. However, while designing and implementing a UML formal semantics translator, the XMI file exported from dynamic UML diagrams have to be parsed, so formal semantics generation algorithm is tightly related with the XMI labels that stores key data/structure information.In this paper, we not only propose the operational semantics and translation rules for UML diagrams in high abstract level, but also pull out the key XMI labels, define their data structure, and propose the formal semantics generation algorithm based on XMI in low abstract level.4. Design and implement UML formal semantics translator meta-tools.We design and implement a set of UML formal semantics translator meta-tools by Java and Xerces parser in Eclipse IDE. UML state/sequence diagrams are assigned with LTS formal semantics or probability/stochastic Kripke formal semantics, and translated to pi-calculus specification or PRISM specification.Multi-level architecture is adopted in software meta-tools:XMI file parser→key data/structure information storage→formal semantics generation→formal specification translation, which enhances the robustness, portability and extendibility of the UML formal semantics translator meta-tools.
|
PDF Full Text Request