嵌入偏序約簡的狀態事件線性時序邏輯驗證

摘要：模型檢驗是硬件和軟件形式化驗證最成功的技術之一.目前大部分的模型檢驗技術是基于狀態的而不考慮遷移上的操作和事件.這導致模型檢驗在驗證使用事件進行交互的組件系統中面臨新的困難,因此需要新的規約技術對狀態事件系統進行規約.狀態事件線性時序邏輯(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的?