嵌入偏序约简的状态事件线性时序逻辑验证  

State/Event Linear Temporal Logic Verification with the Integration of Partial Order Reduction

作　　者：谢健[1] 阚双龙[1] 黄志球[1] 王飞[1] 杨志斌[1] 李伟湋[2] XIE Jian;KAN Shuang-Long;HUANG Zhi-Qiu;WANG Fei;YANG Zhi-Bin;LI Wei-Wei(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016;College of Astronautics,Nanjing University of Aeronautics and Astronautics,Nanjing 210016)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]南京航空航天大学航天学院,南京210016

出　　处：《计算机学报》2019年第10期2145-2159,共15页Chinese Journal of Computers

基　　金：国家高技术研究发展计划项目（2015AA105303）;国家重点研发计划项目(2016YFB1000802）;江苏省自然科学基金青年基金（BK20170809）;中国博士后基金面上基金（2018M632304）资助

摘　　要：模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的�Model checking is one of the most successful formal techniques for verifying hardware and software systems.Most of the model checking techniques are state-based,that is,events and actions on the transitions are not under consideration.However,problems arise when verifying component based systems with model checking,in which the communication among components are data dependent events.Therefore,the formal specification techniques for state/event systems are required.State/Event Linear Temporal Logic(SE-LTL)is a natural and concise way to formal specify a system property,which include both states and events.In SE-LTL,both states and events are viewed as atomic propositions.Model Checking based on automata-theoretic for Linear Temporal Logic(LTL)can be used to verify SE-LTL properties automatically.However,most SE-LTL formulas are not preserved under classic stutter-equivalent relations.Therefore,they cannot be verified with classic Partial Order Reduction(POR),which is one of the most efficiency state space reduction techniques for concurrent systems.In this paper,we propose a novel technique,which is to exploit classical POR to reduce the number of states and transitions of systems during the verification of SE-LTL formulas.It consists of two parts:the first part concentrates on the state space reduction with respect to SE-LTL formulas without NEXT operators and the second part concentrates on the state space reduction with respect to SE-LTL formulas with NEXT operators.The main idea of the first part lies at detecting state parts from Büchi Automata(BA)translated from SE-LTL formulas.State parts means that this part is only related to the states of the systems.Based on the state parts,we propose a Synchronous Product(SP)of a BA and a Labeled Kripke Structure(LKS),which is used to model the behavior of the system.During the construction of the SP,POR is integrated in the construction to reduce the state space of the SP.In other words,POR reduces the state spaces in on-the-fly manner.The integrated POR is modified

关 键 词：偏序约简 状态事件线性时序逻辑 模型检验 同步乘 标签Kripke结构 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]