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

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

模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(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的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.

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 by introducing a visible action detection with respect to the events appearing in SE-LTL formulas.In order to apply the technique to the full class of SE-LTL,we extend the technique for the formulas with NEXT operators,which are another obstacle for POR.This is the second part of our work.The technique detects POR-components in a BA,which can be verified by POR.This technique is also in on-the-fly manner and mixed with the detection of state-transitions.In order to evaluate the efficiency of the technique,we have implemented our techniques into SPIN model checker,which is a tool for verifying concurrent system with respect to classic LTL.The implementation includes the translation from SE-LTL formulas and the on-the-fly state space reductions.The experiments are conducted on three benchmarks:the producer-consumer models,the dinning philosopher problem,and the GIOP protocol in the common object request broker architecture(CORBA).The experimental results show that compared with the pure state-based model checking with POR and SE-LTL model checking without POR,our technique is more efficient and promising and can be used for the verification of state/event systems,especially safety-critical embedded systems.