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

Stochastic Model Checking Continuous Time Markov Process

作　　者：钮俊[1,2,3] 曾国荪[1,2] 吕新荣[3] 徐畅[3] 

机构地区：[1]同济大学计算机科学与技术系,上海201804 [2]嵌入式系统与服务计算教育部重点实验室,上海201804 [3]浙江工商职业技术学院信息工程学院,宁波315012

出　　处：《计算机科学》2011年第9期112-115,125,共5页Computer Science

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

摘　　要：功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信。连续时间Markov决策过程CTMDP(Continu-ous-time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用CT-MDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC(Markov Reward Model Checker)实现模型检测。理论分析表明,提出的针对CTMDP模型的验证需求是必要的,验证思路和方法具有可行性。The trustworthiness of a dynamic system includes the correctness of function and the satisfiability of performance mainly.This paper proposed an approach to verify the function and performance of a system under consideration integratedly.Continuous-time Markov decision process（CTMDP） is a model that contains some aspects such as probabilistic choice,stochastic timing and nondeterminacy,and it is the model by which we verify function properties and analyze performance properties uniformly.We can verify the functional and performance specifications by computing the reachability probabilities in the product CTMDP.We proved the correctness of our approach,and obtained our verification results by using model checker MRMC（Markov Reward Model Checker）.The theoretical results show that model checking CTMDP model is necessary and the model checking approach is feasible.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]