博文
Formal semantics of UML state diagram and automatic verification Based on Kripke
|||
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
https://blog.sciencenet.cn/blog-107188-246058.html
上一篇：ISECS 2009的qq群
下一篇：基于扩展UML 状态图和Markov 过程的系统性能分析
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
https://blog.sciencenet.cn/blog-107188-246058.html
上一篇：ISECS 2009的qq群
下一篇：基于扩展UML 状态图和Markov 过程的系统性能分析
