基本并行进程活性的限界模型检测
作者:
作者单位:

作者简介:

谭锦豪(1996-),男,硕士生,CCF学生会员,主要研究领域为形式化验证,程序语言理论;李国强(1979-),男,博士,副教授,CCF高级会员,主要研究领域为形式化方法,程序语言理论,知识表示与推理.

通讯作者:

李国强,E-mail:li.g@sjtu.edu.cn

中图分类号:

基金项目:

国家自然科学基金(61872232,61732013)


Bounded Model Checking Liveness on Basic Parallel Processes
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61872232, 61732013)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    基本并行进程是一个用于描述和分析并发程序的模型,是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑,其中的AF算子表示从当前的状态出发性质最终会被满足,因此EG逻辑是能够表达活性的逻辑.然而,基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此,提出了基本并行进程上EG逻辑的限界模型检测方法.首先给出了基本并行进程上EG逻辑的限界语义,然后采用基于约束的方法,将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题,最后利用SMT求解器进行求解.

    Abstract:

    Basic parallel process (BPP) is a model for describing and analyzing concurrent programs, which is an important subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPP is undecidable. This study proposes an algorithm for the problem of bounded model checking EG over BPP. First, a bounded semantics of EG over BPP is proposed. Then, according to the constraint-based approach, a reduction from the problem of bounded model checking EG over BPP to the satisfiability problem of linear integer arithmetic formulas is given. Finally, the linear integer arithmetic formulas are solved by SMT solvers.

    参考文献
    相似文献
    引证文献
引用本文

谭锦豪,李国强.基本并行进程活性的限界模型检测.软件学报,2020,31(8):2388-2403

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2019-08-27
  • 最后修改日期:2019-11-02
  • 录用日期:
  • 在线发布日期: 2020-04-20
  • 出版日期: 2020-08-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号