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

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

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

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

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