基于SMT的PTACTL限界模型检测方法

• 作者: 徐亮 毛良文
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 限界模型检测 概率实时系统 概率时间自动机 PTACTL SMT
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件工程
• 页码范围: 41-45
• 页数: 5页
• 分类号: TP301
• 字数: 5322字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2016.03.009

摘要

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性.本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证.通过2个实例说明检测过程的有效性和高效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	毛良文		2	3	1.0	1.0
2	徐亮	湖南师范大学数学与计算机科学学院	9	50	3.0	7.0