首页 | 本学科首页   官方微博 | 高级检索  
     

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

关 键 词:限界模型检测  概率实时系统  概率时间自动机  PTACTL  SMT  
收稿时间:2016-03-17

Bounded Model Checking of PTACTL Based on SMT
MAO Liang-wen,XU Liang.Bounded Model Checking of PTACTL Based on SMT[J].Computer and Modernization,2016,0(3):41-172.
Authors:MAO Liang-wen  XU Liang
Abstract:Probabilistic timed automata are an extension of timed automata with discrete transition probabilities, and can be used to model timed randomized protocols or fault-tolerant systems. We present a bounded model checking method on SMT for verifying probabilistic timed automata against PTACTL properties. This method adds the transition times and transition probabilities into the ACTL properties and changes the encodings of models and properties in order to verify them, which is come from the SMT-based bounded model checking. We also give two examples to show that this method is effectiveness and efficiency.
Keywords:bounded model checking  probabilistic timed systems  probabilistic timed automata  PTACTL  SMT  
点击此处可从《计算机与现代化》浏览原始摘要信息
点击此处可从《计算机与现代化》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号