Paper: Formal semantics of UML state diagram and automatic verification Based on Kripke structure
Author: Yefei Zhao, Zongyuan Yang, Jinkui Xie
Abstract: If UML is formalized with dynamic semantics, automatic verification can be performed for system model in the early stage of software procedure. It becomes more and more important to apply model
checking in UML, such that software architecture can be formalized with dynamic semantics. We explicitly proposed the mapping rules between UML state diagram and Kripke structure semantics. UML state
diagram is mapped to the value transition of variable rather than the transition of states, thus the situation in that system finite state automata can’t be exhausted can be resolved. Finally, a critical
resource competition example is illustrated according to the theory. The mapping rules we proposed are bi-direction, as a result, the theory can be applied in both forward software engineering in design
phase and reverse software engineering in implementation phase.
Published in Conference: 22nd IEEE Canadian Conference on Electrical and Computer Engineering (CCECE 2009)(EI index)
Date: May, 2009
Related Posts
- Pi-calculus based assembly mechanism of UML state diagram and Validation of model refinement
- Formal model and analysis of sliding window protocol based on NuSMV
- Researchers Uncover Scaffolds in the Brain’s Wiring Diagram
- The Minkowski Diagram and the Misrepresentation of Spacetime
- Liveblogging Experimental Pragmatics
Comments are closed.