摘要：模型檢驗是硬件和軟件形式化驗證最成功的技術(shù)之一.目前大部分的模型檢驗技術(shù)是基于狀態(tài)的而不考慮遷移上的操作和事件.這導(dǎo)致模型檢驗在驗證使用事件進行交互的組件系統(tǒng)中面臨新的困難,因此需要新的規(guī)約技術(shù)對狀態(tài)事件系統(tǒng)進行規(guī)約.狀態(tài)事件線性時序邏輯(State/Event Linear Temporal Logic,SE-LTL)給出了一種簡潔和直接的方式表達包含狀態(tài)和事件的系統(tǒng)屬性.在SE-LTL中,狀態(tài)和事件都可以作為原子命題.基于自動機理論的線性時序邏輯(Linear Temporal Logic,LTL)模型檢驗可以被用來對SE-LTL屬性進行驗證.然而SE-LTL屬性在經(jīng)典的stutter等價(stutter-equivalent)下無法保持,所以最有效的并發(fā)程序狀態(tài)約簡技術(shù):偏序約簡技術(shù)(Partial Order Reduction,POR)不能直接應(yīng)用于SE-LTL的驗證.該文提出一種新的方法利用已有的偏序約簡技術(shù)對SE-LTL驗證過程的狀態(tài)空間進行約簡.該方法分為兩個部分:第一個部分是針對SE-LTL不帶NEXT算子的約簡方法;第二部分則是帶NEXT算子的約簡方法.第一部分的主要思想是從一個Büchi自動機(Automata,BA)中抽取出“狀態(tài)部分”.“狀態(tài)部分”的含義是該部分只與系統(tǒng)的狀態(tài)相關(guān).基于“狀態(tài)部分”,給出關(guān)于BA和標簽Kripke結(jié)構(gòu)(Labeled Kripke Structure)的同步乘,并在同步乘的構(gòu)造過程中嵌入偏序約簡技術(shù),從而約簡同步乘的狀態(tài)空間,即該文的約簡技術(shù)是on-the-fly的.嵌入的偏序約簡在已有的偏序約簡基礎(chǔ)上,面向SE-LTL公式中的事件引入新的可見操作的識別方法.為了能夠?qū)⑵蚣s簡技術(shù)應(yīng)用到所有的SE-LTL公式,該文同時給出驗證SE-LTL帶NEXT算子的偏序約簡算法.NEXT算子是偏序約簡的另一個主要障礙.該部分是文中的第二部分工作.該部分的技術(shù)依然是on-the-fly的,并且需要與狀態(tài)部分的識別相結(jié)合.通過將該文技術(shù)實現(xiàn)到SPIN模型檢驗器中對已有的模型進行驗證.Spin是針對LTL的?