《计算机学报》文章摘要   全文下载
文章题目	基于模型检测的时间空间性能验证方法
作者	钮俊1),2),3) 曾国荪1),2) 王伟1),2)
作者单位	1)(同济大学计算机科学及技术系 上海 201804) 2)(嵌入式系统与服务计算教育部重点实验室 上海 201804) 3)(浙江工商职业技术学院信息工程学院 浙江 宁波 315012)
发表年份	2010
发表月份	9期(1621—1633)
文章摘要	摘要 对具有不确定性的复杂系统如网络协议等的性能进行分析是当前的研究热点.将空间资源分析纳入到性能评估过程，用模型检测技术验证时间或空间性能是否满足期望的需求约束.用能刻画不确定性的连续时间Markov回报过程(Continuous-Time Markov Reward Process,CTMRP)作为时间或空间性能验证模型；用正则式表示路径约束，扩展连续随机回报逻辑CSRL(Continuous Stochastic Reward Logic)的时态路径算子，用以刻画更加广泛的基于状态或路径的时间或空间性能验证属性；提出并证明CTMRP在确定性策略下空间时间可达概率的对偶性质，将带有约束的空间性能验证最终转化为时间性能的可达分析，给出验证算法.文中的结论和算法为复杂系统的性能分析提供了新的思路和方法. 关键词 不确定性；模型检测；时间空间性能；可达概率；对偶 中图法分类号 TP301 DOI号：10.3724/SP.J.1016.2010.01621