廣義反應(yīng)式系統(tǒng)形式開(kāi)發(fā)方法研究.pdf

1、重慶大學(xué)博士學(xué)位論文廣義反應(yīng)式系統(tǒng)形式開(kāi)發(fā)方法研究姓名：張廣泉申請(qǐng)學(xué)位級(jí)別：博士專業(yè)：計(jì)算機(jī)軟件與理論指導(dǎo)教師：沈一棟19990601博士學(xué)位論文III!s!!!!!j!!!!!!!E!!I自自_自自!!!!!!!!!!EE!!!!!!!s!!!!!!!!!!!!!!!!!!!E!!!E本文給出基于轉(zhuǎn)換系統(tǒng)的不同擴(kuò)充形式，作為三類反應(yīng)式系統(tǒng)的計(jì)算模型：采用時(shí)態(tài)邏輯PLTL及其擴(kuò)充形式作為三類反應(yīng)式系統(tǒng)的形式化描述語(yǔ)言。對(duì)上述問(wèn)題，進(jìn)行了

2、系統(tǒng)而深入的研究，取得了如下主要結(jié)果：，，(1)針對(duì)上述第一類問(wèn)題，提出并發(fā)模型PTS的一種粒度分析方法竅f入一種限制臨界引用(LCR)條件，對(duì)任一程序，通過(guò)轉(zhuǎn)換算法將其轉(zhuǎn)化為與之等價(jià)的LcR程序，且LCR程序的交替計(jì)算結(jié)果與實(shí)際的重疊執(zhí)行結(jié)果是一致的，解決了FTS模型的交替計(jì)算形式與實(shí)際系統(tǒng)的重疊執(zhí)行形式之間不一致的問(wèn)題。本文的分析和討論為交替模型的進(jìn)一步應(yīng)用提供了一個(gè)理論基礎(chǔ)卜一，(2)針對(duì)第二類問(wèn)題，對(duì)并發(fā)程序及其性質(zhì)進(jìn)行系統(tǒng)地描

3、述和分類。務(wù)出了并發(fā)性質(zhì)的形式化定義方法，并根據(jù)PLTL時(shí)態(tài)公式的不同形式，對(duì)并發(fā)性質(zhì)進(jìn)行細(xì)致地分類。本文的工作有利于深入分析并發(fā)程序不同的性質(zhì)特征及相互之間的關(guān)系，并為下一步系統(tǒng)驗(yàn)證工作奠定了良好的基礎(chǔ)|卜／一j。(3)針對(duì)第三類問(wèn)題，提出一種基于公平性假設(shè)的時(shí)態(tài)邏輯技術(shù)描述AB協(xié)議／臊用的時(shí)態(tài)邏輯方法由轉(zhuǎn)換系統(tǒng)、一組公平性需求及一組公理構(gòu)成，不但求精過(guò)程直觀、簡(jiǎn)單，而且也易于協(xié)議的驗(yàn)證，克服了目前絕大多數(shù)FDT在處理協(xié)議的活性及逐步

4、求精等方面存在的不足。(4)針對(duì)第四類問(wèn)題，提出了基于PLTL的并發(fā)程序的兩種驗(yàn)證方法并給出相應(yīng)實(shí)例系。j統(tǒng)的驗(yàn)證、脅提出一種基于修改的∞一自動(dòng)機(jī)和公平轉(zhuǎn)換系統(tǒng)FTS相結(jié)合的圖驗(yàn)證方法，。該方法可證明任何形式的時(shí)態(tài)公式表示的并發(fā)程序性質(zhì)，因而具有廣泛的適用性②提出一種基于PLTL的模型檢驗(yàn)算法，該算法不但能驗(yàn)證安全性，也能驗(yàn)證活性，并且對(duì)時(shí)態(tài)公式的形式?jīng)]有限制，因而更具一般性和廣泛性。卜一～7(5)對(duì)第五類PI題，由于PLTL描述語(yǔ)言與

5、PTS建模工具只適合于并發(fā)系統(tǒng)，而不能表示實(shí)時(shí)及混合系統(tǒng)基于此，本文的工作是：①通過(guò)擴(kuò)充FTS，提出了一種改進(jìn)的TTM一一實(shí)時(shí)轉(zhuǎn)換模型：引入時(shí)間因子到PLTL，提出了一種定量時(shí)態(tài)邏輯；②通過(guò)擴(kuò)充FTS，提出混合系統(tǒng)的一種新的計(jì)算模型一一混合轉(zhuǎn)換系統(tǒng)IITS，給出混合系統(tǒng)描述的一種擴(kuò)充時(shí)態(tài)邏輯本文初步探討了實(shí)時(shí)及混合系統(tǒng)的描述和建模問(wèn)題本文的研究工作得到國(guó)家自然科學(xué)基金、四川省教委青年科研基金及重慶市應(yīng)用基礎(chǔ)研究項(xiàng)目資助。關(guān)鍵詞：反應(yīng)系統(tǒng)