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

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

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

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

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

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