|
|||||
|
|
| 基于SMT的PTACTL限界模型检测方法 | |
| 作者姓名： | 毛良文 徐亮 |
| 基金项目： | 国家自然科学基金资助项目(61502165); 湖南省科技计划项目(2014FJ6030); 湖南省教育厅科研项目(13C527); 长沙市科技计划项目(k1403042-11); 湖南省重点学科建设项目(湘教发[2011]76号); 湖南师范大学学位与研究生教育教改课题(14JG13); 湖南师范大学教学改革项目(处发2015-13-52) |
| 摘 要： | 概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。 |
| 关 键 词： | 限界模型检测 概率实时系统 概率时间自动机 PTACTL SMT |
| 收稿时间： | 2016-03-17 |
| 点击此处可从《计算机与现代化》浏览原始摘要信息 | |
| 点击此处可从《计算机与现代化》下载全文 | |