版权所有：内蒙古大学图书馆 技术提供：维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
基于SMT的PTACTL限界模型检测方法
Bounded Model Checking of PTACTL Based on SMT作者机构：湖南省产商品质量监督检验研究院湖南长沙410007 湖南师范大学数学与计算机科学学院湖南长沙410081 高性能计算与随机信息处理省部共建教育部重点实验室湖南长沙410081
出 版 物：《计算机与现代化》 (Computer and Modernization)
年 卷 期：2016年第3期
页 面：41-45页
学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金资助项目(61502165) 湖南省科技计划项目(2014FJ6030) 湖南省教育厅科研项目(13C527) 长沙市科技计划项目(k1403042-11) 湖南省重点学科建设项目(湘教发76号) 湖南师范大学学位与研究生教育教改课题(14JG13) 湖南师范大学教学改革项目(处发2015-13-52)
主 题：限界模型检测 概率实时系统 概率时间自动机 PTACTL SMT
摘 要：概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。
