摘要:展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明:当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,对影响反向展开效率的关键因素做了分析与总结.
Abstract:Unfolding technology can partially alleviate the state explosion problem in Petri net through branching processes. However, an unfolding still contains all states of a system. Some practical problems only need to determine the coverability of a specific state, which is expected to reduce the scale of unfolding net. This study proposes a target-oriented reverse unfolding algorithm for the coverability problem of 1-safe Petri nets, which combines heuristic technology to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding technology is applied to the formal verification of concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/6240
删除或更新信息,请邮件至freekaoyan#163.com(#换成@)
Petri网的反向展开及其在程序数据竞争检测的应用
本站小编 Free考研考试/2022-01-02
相关话题/系统 技术 程序 信息 实验
面向SPARC处理器架构的操作系统异常管理验证
摘要:航天器等安全关键系统是典型的嵌入式系统,具有多任务并发、中断频发等特点.操作系统是其最基础的软件,构建一个正确的操作系统是保障航天器系统高可信运行的关键.异常管理作为操作系统最底层的功能,负责引导系统控制流的突变来响应处理器状态中的某些变化,异常管理的正确性是整个操作系统正确性的基础.提出一种 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于锁增广分段图的多线程程序死锁检测
摘要:死锁是并行程序常见的缺陷之一,动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而,锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行,扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息,分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向持续软件工程的微服务架构技术专题前言
摘要:随着软件互联网化和服务化的高度发展,持续性(continuity)成为现代软件系统的基本特性之一,覆盖从商业策划、软件开发、运维、演化的所有环节,使得软件系统在持续稳定提供功能和服务的同时,软件系统的边界和内部结构始终处于不断变化、持续更新和适应之中,持续软件工程(continuoussoft ...中科院软件研究所 本站小编 Free考研考试 2022-01-02一种监控系统的链路跟踪型日志数据的存储设计
摘要:随着软件系统越来越复杂化和分布化,为系统提供具有完善功能的监控服务显得越来越重要.APM(applicationperformancemanagement)系统通过采集软件系统运行时的各项指标数据来分析软件的运行状态,例如CPU、内存使用率、垃圾回收的耗时、QPS等指标.此外,APM系统也会在 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02多版本共存的微服务系统自适应演化方法
摘要:微服务设计模式通过将应用程序拆分成多个相互独立的微服务,实现了各个微服务之间的相互解耦,允许各个微服务能够独立地进行迭代开发、部署,从而对用户需求变化以及DevOps流程中部署需求作出快速响应.每个微服务的独立迭代升级导致了系统中可能出现多版本共存现象,不同服务的不同版本之间的依赖关系变得更加 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02程序智能合成技术研究进展
摘要:近年来,随着信息技术快速发展,软件重要性与日俱增,极大地推动了国民经济的发展.然而,由于软件业务形态越来越复杂和需求变化越来越快,软件的开发和维护成本急剧增加,迫切需要探索新的软件开发模式和技术.目前,各行业在软件活动中积累了规模巨大的软件代码和数据,这些软件资产为软件智能化开发建立了数据基础 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02轨迹表示学习技术研究进展
摘要:基于地理位置信息的应用和服务的迅速发展,对轨迹数据挖掘提出了新的需求和挑战.原始轨迹数据通常是由坐标-时间戳元组构成的有序序列,而现有的大多数数据分析算法均要求输入数据位于向量空间中.因此,为了将轨迹数据从变长的坐标-时间戳序列转化成定长的向量表示且保持原有的特征,对轨迹数据进行有效的表示是十 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02区块链系统攻击与防御技术研究进展
摘要:区块链作为一种多技术融合的新兴服务架构,因其去中心化、不可篡改等特点,受到了学术界和工业界的广泛关注.然而,由于区块链技术架构的复杂性,针对区块链的攻击方式层出不穷,逐年增加的安全事件导致了巨大的经济损失,严重影响了区块链技术的发展与应用.从层级分类、攻击关联分析两个维度对区块链已有安全问题的 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向领域的软件系统构造与质量保障专题前言
摘要:软件是推动新一代信息技术发展的驱动力.随着互联网、云计算、人工智能等技术的快速发展,软件与物联网、区块链、自动驾驶等众多领域的融合进一步加强,正引领并促进这些领域向数字化、智能化发展,为社会、经济的加速演进和创新发展带来了新的契机.因此,面向领域的软件技术不仅是软件领域,也是众多其他领域国内外 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于环境建模的物联网系统TAP规则生成方法
摘要:用户需求是物联网智能服务的根本驱动力,如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程(TAP)规则进行编程,但它们描述的是设备调度程序,并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法,支持服务目标的分解,但很难保证物联网不同服务间的一致性和服务部署的完整性.为了支持 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02