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

• 作者: 吕新荣 徐畅 曾国荪 钮俊
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 功能性能 连续时间Markov决策过程 模型检测 可信验证 可达概率
• 年，卷（期）: 2011,（9）
• 所属期刊栏目: 软件工程
• 页码范围: 112-115,125
• 分类号: TP301
• 字数: 7413字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2011.09.025

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钮俊	同济大学计算机科学与技术系	7	59	4.0	7.0
10	曾国荪	同济大学计算机科学与技术系	102	1102	17.0	29.0
14	吕新荣	浙江工商职业技术学院信息工程学院	11	23	4.0	4.0
15	徐畅	浙江工商职业技术学院信息工程学院	39	63	4.0	6.0