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

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

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

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

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