基于抽象解釋的時(shí)間多棧下推網(wǎng)絡(luò)研究.pdf

1、基于模型檢測(cè)的實(shí)時(shí)并發(fā)系統(tǒng)的驗(yàn)證一直是業(yè)界的研究熱點(diǎn)。針對(duì)實(shí)時(shí)系統(tǒng)中的時(shí)間因子的復(fù)雜性，諸多學(xué)者提出了如時(shí)間自動(dòng)機(jī)，時(shí)間下推自動(dòng)機(jī)和時(shí)間下推網(wǎng)絡(luò)等模型來驗(yàn)證實(shí)時(shí)并發(fā)系統(tǒng)的正確性等問題，但是由于連續(xù)的時(shí)間模型會(huì)導(dǎo)致狀態(tài)空間爆炸問題。本文基于抽象解釋理論形式化地分析研究時(shí)間多棧下推網(wǎng)絡(luò)（TMPDN）。抽象解釋理論由P.Cousot和R.Cousot在1977年提出，其目標(biāo)是在程序靜態(tài)分析時(shí)構(gòu)造和逼近程序不動(dòng)點(diǎn)語義。為了使用抽象解釋理論形式化

2、分析TMPDN模型，構(gòu)建出TMPDN模型的具體域，然后通過時(shí)間域和時(shí)間帶兩種方法找到相應(yīng)的抽象域，并建立具體域和抽象域之間的Galois連接。然后構(gòu)建出具體域中的具體計(jì)算步驟和對(duì)應(yīng)的時(shí)間域抽象域中的抽象計(jì)算步驟和對(duì)應(yīng)的時(shí)間域抽象域中的抽象計(jì)算步驟，其中具體計(jì)算步驟描述具體格局的遷移函數(shù)△，抽象計(jì)算步驟描述時(shí)間域抽象域和時(shí)間帶抽象域的抽象格局遷移函數(shù)△＃，通過抽象解釋理論中的二元抽象方式建立具體計(jì)算步驟f:C→C與抽象計(jì)算步驟f#:A→A

3、之間的抽象方式。最后給出基于抽象解釋的時(shí)間多棧下推網(wǎng)絡(luò)的抽象方式的可靠性證明。
　　本研究主要內(nèi)容包括：⑴根據(jù)時(shí)間多棧下推網(wǎng)絡(luò)（TMPDN）的構(gòu)造方法和抽象解釋理論框架的定義，提出時(shí)間多棧下推網(wǎng)絡(luò)（TMPDN）的具體格局和具體域模型。引入時(shí)間域的概念，并基于時(shí)間域構(gòu)造Galois連接找到時(shí)間多棧下推網(wǎng)絡(luò)（TMPDN）的具體格局和具體域所對(duì)應(yīng)的時(shí)間域抽象格局和時(shí)間域抽象域。⑵在時(shí)間域的基礎(chǔ)上給出時(shí)間帶的概念，并基于時(shí)間帶構(gòu)造Galo

4、is連接找到時(shí)間多棧下推網(wǎng)絡(luò)（TMPDN）的時(shí)間帶具體格局和時(shí)間帶具體域所對(duì)應(yīng)的時(shí)間帶抽象格局和時(shí)間帶抽象域。⑶構(gòu)建出具體域中的具體計(jì)算步驟（concrete computation step）和對(duì)應(yīng)的時(shí)間域抽象域中的抽象計(jì)算步驟（abstract computation step），其中具體計(jì)算步驟描述具體格局的遷移函數(shù)△，抽象計(jì)算步驟描述時(shí)間域抽象域和時(shí)間帶抽象域的抽象格局遷移函數(shù)△#，通過抽象解釋理論中的二元抽象方式建立具體計(jì)算步