| 基于模型检测的时间空间性能验证方法 |
| |
| 引用本文： | 钮俊,曾国荪,王伟.基于模型检测的时间空间性能验证方法[J].计算机学报,2010,33(9). |
| |
| 作者姓名： | 钮俊 曾国荪 王伟 |
| |
| 作者单位： | 1. 同济大学计算机科学及技术系,上海,201804;嵌入式系统与服务计算教育部重点实验室,上海,201804;浙江工商职业技术学院信息工程学院,浙江,宁波,315012
2. 同济大学计算机科学及技术系,上海,201804;嵌入式系统与服务计算教育部重点实验室,上海,201804 |
| |
| 基金项目： | 国家"八六三"高技术研究发展计划项目基金，国家"九七三"重点基础研究发展规划项目基金，国家自然科学基金，NSFC-微软亚洲研究院联合项目，教育部博士点基金，上海市优秀学科带头人计划项目，高效能服务器和存储技术国家重点实验室开放基金，同济大学青年优秀人才培养行动计划，浙江省宁波市自然科学基金 |
| |
| 摘 要： | 对具有不确定性的复杂系统如网络协议等的性能进行分析是当前的研究热点.将空间资源分析纳入到性能评估过程,用模型检测技术验证时间或空间性能是否满足期望的需求约束.用能刻画不确定性的连续时间Markov回报过程(Continuous-Time Markov Reward Process,CTMRP)作为时间或空间性能验证模型;用正则式表示路径约束,扩展连续随机回报逻辑CSRL(Continuous Stochastic Reward Logic)的时态路径算子,用以刻画更加广泛的基于状态或路径的时间或空间性能验证属性;提出并证明CTMRP在确定性策略下空间时间可达概率的对偶性质,将带有约束的空间性能验证最终转化为时间性能的可达分析,给出验证算法.文中的结论和算法为复杂系统的性能分析提供了新的思路和方法.
|
| 关 键 词： | 不确定性 模型检测 时间空间性能 可达概率 对偶 |
An Approach of Model Checking Time or Space Performance |
| |
| NIU Jun,ZENG Guo-Sun,WANG Wei.An Approach of Model Checking Time or Space Performance[J].Chinese Journal of Computers,2010,33(9). |
| |
| Authors: | NIU Jun ZENG Guo-Sun WANG Wei |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
