基于模型检测的时间空间性能验证方法

• 作者: 曾国荪 王伟 钮俊
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 不确定性 模型检测 时间空间性能 可达概率 对偶
• 年，卷（期）: 2010,（9）
• 页码范围: 1621-1633
• 分类号: TP301
• 字数: 14914字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2010.01621

摘要

对具有不确定性的复杂系统如网络协议等的性能进行分析是当前的研究热点.将空间资源分析纳入到性能评估过程,用模型检测技术验证时间或空间性能是否满足期望的需求约束.用能刻画不确定性的连续时间Markov回报过程(Continuous-Time Markov Reward Process,CTMRP)作为时间或空间性能验证模型;用正则式表示路径约束,扩展连续随机回报逻辑CSRL(Continuous Stochastic Reward Logic)的时态路径算子,用以刻画更加广泛的基于状态或路径的时间或空间性能验证属性;提出并证明CTMRP在确定性策略下空间时间可达概率的对偶性质,将带有约束的空间性能验证最终转化为时间性能的可达分析,给出验证算法.文中的结论和算法为复杂系统的性能分析提供了新的思路和方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钮俊	同济大学计算机科学及技术系	7	59	4.0	7.0
10	曾国荪	同济大学计算机科学及技术系	102	1102	17.0	29.0
14	王伟	同济大学计算机科学及技术系	238	3083	28.0	47.0