首頁(yè) > 期刊 > 自然科學(xué)與工程技術(shù) > 信息科技 > 電子信息科學(xué)綜合 > 計(jì)算機(jī)學(xué)報(bào) > 嵌入偏序約簡(jiǎn)的狀態(tài)事件線性時(shí)序邏輯驗(yàn)證 【正文】
嵌入偏序約簡(jiǎn)的狀態(tài)事件線性時(shí)序邏輯驗(yàn)證
- 偏序約簡(jiǎn)
- 狀態(tài)事件線性時(shí)序邏輯
- 模型檢驗(yàn)
- 同步乘
- 標(biāo)簽kripke結(jié)構(gòu)
摘要：模型檢驗(yàn)是硬件和軟件形式化驗(yàn)證最成功的技術(shù)之一.目前大部分的模型檢驗(yàn)技術(shù)是基于狀態(tài)的而不考慮遷移上的操作和事件.這導(dǎo)致模型檢驗(yàn)在驗(yàn)證使用事件進(jìn)行交互的組件系統(tǒng)中面臨新的困難,因此需要新的規(guī)約技術(shù)對(duì)狀態(tài)事件系統(tǒng)進(jìn)行規(guī)約.狀態(tài)事件線性時(shí)序邏輯(State/Event Linear Temporal Logic,SE-LTL)給出了一種簡(jiǎn)潔和直接的方式表達(dá)包含狀態(tài)和事件的系統(tǒng)屬性.在SE-LTL中,狀態(tài)和事件都可以作為原子命題.基于自動(dòng)機(jī)理論的線性時(shí)序邏輯(Linear Temporal Logic,LTL)模型檢驗(yàn)可以被用來(lái)對(duì)SE-LTL屬性進(jìn)行驗(yàn)證.然而SE-LTL屬性在經(jīng)典的stutter等價(jià)(stutter-equivalent)下無(wú)法保持,所以最有效的并發(fā)程序狀態(tài)約簡(jiǎn)技術(shù):偏序約簡(jiǎn)技術(shù)(Partial Order Reduction,POR)不能直接應(yīng)用于SE-LTL的驗(yàn)證.該文提出一種新的方法利用已有的偏序約簡(jiǎn)技術(shù)對(duì)SE-LTL驗(yàn)證過(guò)程的狀態(tài)空間進(jìn)行約簡(jiǎn).該方法分為兩個(gè)部分:第一個(gè)部分是針對(duì)SE-LTL不帶NEXT算子的約簡(jiǎn)方法;第二部分則是帶NEXT算子的約簡(jiǎn)方法.第一部分的主要思想是從一個(gè)Büchi自動(dòng)機(jī)(Automata,BA)中抽取出“狀態(tài)部分”.“狀態(tài)部分”的含義是該部分只與系統(tǒng)的狀態(tài)相關(guān).基于“狀態(tài)部分”,給出關(guān)于BA和標(biāo)簽Kripke結(jié)構(gòu)(Labeled Kripke Structure)的同步乘,并在同步乘的構(gòu)造過(guò)程中嵌入偏序約簡(jiǎn)技術(shù),從而約簡(jiǎn)同步乘的狀態(tài)空間,即該文的約簡(jiǎn)技術(shù)是on-the-fly的.嵌入的偏序約簡(jiǎn)在已有的偏序約簡(jiǎn)基礎(chǔ)上,面向SE-LTL公式中的事件引入新的可見操作的識(shí)別方法.為了能夠?qū)⑵蚣s簡(jiǎn)技術(shù)應(yīng)用到所有的SE-LTL公式,該文同時(shí)給出驗(yàn)證SE-LTL帶NEXT算子的偏序約簡(jiǎn)算法.NEXT算子是偏序約簡(jiǎn)的另一個(gè)主要障礙.該部分是文中的第二部分工作.該部分的技術(shù)依然是on-the-fly的,并且需要與狀態(tài)部分的識(shí)別相結(jié)合.通過(guò)將該文技術(shù)實(shí)現(xiàn)到SPIN模型檢驗(yàn)器中對(duì)已有的模型進(jìn)行驗(yàn)證.Spin是針對(duì)LTL的?
注：因版權(quán)方要求，不能公開全文，如需全文，請(qǐng)咨詢雜志社
計(jì)算機(jī)學(xué)報(bào)
- 預(yù)計(jì)1-3個(gè)月 預(yù)計(jì)審稿周期
- 3.18 影響因子
- 計(jì)算機(jī) 快捷分類
- 月刊 出版周期
主管單位：中國(guó)科學(xué)院;主辦單位：中國(guó)計(jì)算機(jī)學(xué)會(huì);中國(guó)科學(xué)院計(jì)算技術(shù)研究所
我們提供的服務(wù)
在線客服
一對(duì)一咨詢服務(wù)、簡(jiǎn)單快捷、省時(shí)省力
了解更多 >
快遞配送
直郵到家、實(shí)時(shí)跟蹤、更安全更省心
了解更多 >
雜志訂閱
去除中間環(huán)節(jié)享受低價(jià)，物流進(jìn)度實(shí)時(shí)通知
了解更多 >
雜志推薦
正版雜志，匹配度高、性價(jià)比高、成功率高
了解更多 >