随机模型检测连续时间Markov过程

摘要：

功能正确和性能可满足是复杂系统可信要求非常重要的两个方面.从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信.连续时间Markov决策过程CTMDP(Continuous-time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征.提出用CTMDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC(Markov Reward Model Checker)实现模型检测.理论分析表明,提出的针对CTMDP模型的验证需求是必要的,验证思路和方法具有可行性.

关键词：功能性能、连续时间Markov决策过程、模型检测、可信验证、可达概率

所属期刊栏目：38

分类号：TP301(计算技术、计算机技术)

资助基金：863项目2007AA01Z425,2009AA012201;973计划课题2007CB316502;国家自然科学基金项目90718015;NSFC-软亚洲研究院联合资助项目60970155;教育部博士点基金项目20090072110035;上海市优秀学科带头人计划项目10XD1404400;高效能服务器和存储技术国家重点实验室开放基金项目2009HSSA06;浙江省宁波市自然科学基金项目2010A610123;浙江省教育厅科研项目Y201017075

在线出版日期：2012-01-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：112-115,125