计算机与现代化

• 软件工程 • 上一篇    下一篇

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

  

  1. (1.湖南省产商品质量监督检验研究院,湖南 长沙 410007; 2.湖南师范大学数学与计算机科学学院,湖南 长沙 410081; 3.高性能计算与随机信息处理省部共建教育部重点实验室,湖南 长沙 410081)
  • 收稿日期:2015-12-23 出版日期:2016-03-17 发布日期:2016-03-17
  • 作者简介:毛良文(1969-),男,湖南益阳人,湖南省产商品质量监督检验研究院工程师,研究方向:信息系统安全; 通信作者:徐亮(1981-),男,湖南长沙人,湖南师范大学数学与计算机科学学院副教授,博士,研究方向:中文信息处理,安全操作系统。
  • 基金资助:
    国家自然科学基金资助项目(61502165); 湖南省科技计划项目(2014FJ6030); 湖南省教育厅科研项目(13C527); 长沙市科技计划项目(k1403042-11); 湖南省重点学科建设项目(湘教发[2011]76号); 湖南师范大学学位与研究生教育教改课题(14JG13); 湖南师范大学教学改革项目(处发2015-13-52)

Bounded Model Checking of PTACTL Based on SMT

  1. (1. Hunan Testing Institute of Product and Commodity Supervision, Changsha 410007, China; 2. College of Mathematics and Computer Science, Hunan Normal University, Changsha 410081, China; 3. Key Laboratory of High Performance Computing and Stochastic Information Processing, Ministry of Education, Changsha 410081, China)
  • Received:2015-12-23 Online:2016-03-17 Published:2016-03-17

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

关键词: 限界模型检测, 概率实时系统, 概率时间自动机, PTACTL, SMT

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.

Key words: bounded model checking, probabilistic timed systems, probabilistic timed automata, PTACTL, SMT

中图分类号: