一种基于非交互式Petri网的异步程序验证模型和方法
作者:
作者单位:

作者简介:

通讯作者:

李国强,li.g@sjtu.edu.cn

中图分类号:

TP311

基金项目:

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


A formal model and method for verifying asynchronous program based on communication-free Petri net
Author:
Affiliation:

Fund Project:

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

    异步程序使用异步非阻塞调用方式来实现程序的并发,被广泛应用于并行与分布式系统中.验证异步程序复杂性很高,无论是安全性还是活性均达到EXPSPACE难.本文提出一个异步程序的程序模型系统,并在其上定义了两个异步程序上的问题:等价性问题和可达性问题.通过将3-CNF-SAT规约到这两个问题,再将其规约至非交互式Petri网的可达性证明两个问题是NP完备的.案例表明,这两个问题可以解决异步程序上一系列的程序验证问题.

    Abstract:

    Asynchronous programs use asynchronous non-blocking calls to achieve program concurrency, are widely used in parallel and distributed systems. The complexity of verifying asynchronous programs is very high, no matter safety or liveness . This paper proposes a program model of asynchronous programs, and defines two problems on asynchronous programs:the-equivlence problem and reachability problem. By reducing the 3-CNF-SAT to these two problems, and then reducing them to the reachablity problem of communication-free Petri net, we prove that the two problems are both NP-complete. The case shows that these two problems can solve a series of program verification problems on asynchronous programs.

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

吴志文,李国强.一种基于非交互式Petri网的异步程序验证模型和方法.软件学报,,():0

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

京公网安备 11040202500063号