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

  

作者：赵也非，杨宗源，谢瑾奎，刘强

  

摘要：

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

     

关键字：UML 状态图；Markov 过程；PRISM；概率模型检测

  

发表期刊：科技论文在线（精品论文，五颗星）

  

网址：http://www.paper.edu.cn/paper.php?serial_number=200907-446

  

发表日期：2009年8月

  

转载本文请联系原作者获取授权，同时请注明本文来自赵也非科学网博客。
链接地址：https://m.sciencenet.cn/blog-107188-250496.html

上一篇：Formal semantics of UML state diagram and automatic verification Based on Kripke
下一篇：UML序列图的操作语义及其在模型精化中的一致性检查