|国家预印本平台
首页|基于扩展UML状态图和Markov过程的系统性能分析

基于扩展UML状态图和Markov过程的系统性能分析

System performance analysis Based on extended UML state diagram and Markov process

中文摘要英文摘要

把概率模型检测应用于软件架构,可以在模型精化过程中,对基于Markov过程的实时模型,进行功能验证和性能分析,对软件开发设计具有指导作用。本文提出了从扩展UML状态图到概率Kripke结构语义之间的双向映射规则和精确定义,给出了总的形式语义生成算法;以一个异步并发组合的DTMC系统为例,用PCTL表示系统关键非功能属性,用模型检测器实现自动分析验证,给出了理论推导过程,并和实验结果进行了分析比较。本文提出的映射规则是双射的,既可应用于正向工程,又可应用于逆向工程。

If software architecture is formalized with probabilistic model checking, then real-time model based on markov process can be automatically function validated and performance analysised during model refinement, thus the dependability of software design and development is improved. In this paper, we proposed the bi-direction mapping rules and exact definition between UML state diagram and probabibilistic Kripke structrue semantics, as well as the general formal semantics generation algorithm. An asynchronous parallel composited DTMC system is illustrated and the key non-function properties of system are described by PCTL, thus automatic verification and analysis are performed through model checker. We also presented the theory deduction process of the properties and compare it with experiment result. 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.

杨宗源、谢瑾奎、刘强、赵也非

NONE

UML状态图Markov过程PRISM概率模型检测软件确保

UML state diagramMarkov processPRISMProbabilistic model checkingSoftware assurance

杨宗源,谢瑾奎,刘强,赵也非.基于扩展UML状态图和Markov过程的系统性能分析[EB/OL].(2009-07-21)[2025-08-25].http://www.paper.edu.cn/releasepaper/content/200907-446.点此复制

评论