【摘要】：一般硬件系統(tǒng)和軟件系統(tǒng)都存在大量的相同的或同構(gòu)的組件,相應(yīng)地,它們的模型常常在結(jié)構(gòu)上存在對(duì)稱性,這種對(duì)稱結(jié)構(gòu)一般具有相同或非常相近的性質(zhì)。人們?yōu)榱耸箚栴}簡(jiǎn)化,根據(jù)這種情況開發(fā)了對(duì)稱約簡(jiǎn)算法來簡(jiǎn)化模型。特別是在形式化驗(yàn)證中,對(duì)稱約簡(jiǎn)方法已經(jīng)成為解決狀態(tài)爆炸問題的有效方法之一。進(jìn)程代數(shù)已經(jīng)是刻畫并發(fā)系統(tǒng)的最普遍、最常用的描述語言,而事件結(jié)構(gòu)也是刻畫真并發(fā)系統(tǒng)的強(qiáng)有力的建模工具,它們常常展示出對(duì)稱性。然而,當(dāng)前大多數(shù)研究都集中在基于變遷系統(tǒng)模型的對(duì)稱約簡(jiǎn),從未涉及這兩種建模工具的對(duì)稱性方面的研究。在本文中,我們對(duì)進(jìn)程代數(shù)語言和事件結(jié)構(gòu)模型的對(duì)稱約簡(jiǎn)進(jìn)行了深入研究。這些工作力圖從結(jié)構(gòu)上建立對(duì)建模語言和模型進(jìn)行約簡(jiǎn)的基本理論,目的是希望從結(jié)構(gòu)上建立起類似于行為等價(jià)的由細(xì)到粗的約簡(jiǎn)體系,為開發(fā)復(fù)雜系統(tǒng)而建立的不同層次靜態(tài)約簡(jiǎn)模型服務(wù)。另一方面,自頂向下逐步細(xì)化的層次化設(shè)計(jì)方法是人們廣泛接受的設(shè)計(jì)計(jì)算機(jī)硬件系統(tǒng)和軟件系統(tǒng)的最主要方法之一。動(dòng)作細(xì)化是系統(tǒng)層次化刻畫方法的核心操作,這一理論的研究一般在進(jìn)程代數(shù)和事件結(jié)構(gòu)模型中進(jìn)行的,已經(jīng)取得了豐碩的成果。在此基礎(chǔ)上,我們研究了對(duì)稱約簡(jiǎn)對(duì)動(dòng)作細(xì)化的影響,同時(shí)研究了交織等價(jià)和步進(jìn)等價(jià)在動(dòng)作細(xì)化下的保持問題。 本文針對(duì)進(jìn)程代數(shù)語言提出了進(jìn)程的對(duì)稱性概念,給出了對(duì)稱約簡(jiǎn)算法,并證明了約簡(jiǎn)后的進(jìn)程與原進(jìn)程是交織跡和交織互模擬等價(jià)的,同時(shí)提供了兩個(gè)有意義的實(shí)例來說明對(duì)稱性的定義并驗(yàn)證了約簡(jiǎn)算法的正確性。 接下來,針對(duì)事件結(jié)構(gòu)模型我們提出了基于置換群的對(duì)稱性概念。在事件結(jié)構(gòu)中,引入了事件結(jié)構(gòu)的商結(jié)構(gòu)模型,證明了商結(jié)構(gòu)與原事件結(jié)構(gòu)是跡、互模擬和偏序多集跡等價(jià)的,建立了針對(duì)事件結(jié)構(gòu)的對(duì)稱約簡(jiǎn)算法,得出了對(duì)稱約簡(jiǎn)不影響等價(jià)在動(dòng)作細(xì)化下的保持。在研究了事件結(jié)構(gòu)的對(duì)稱性之后,進(jìn)一步從理論上比較對(duì)稱約簡(jiǎn)與自互模擬約簡(jiǎn)的區(qū)別和聯(lián)系。 交織等價(jià)(即交織跡等價(jià)和交織互模擬等價(jià))與步進(jìn)等價(jià)(即步進(jìn)跡等價(jià)和步進(jìn)互模擬等價(jià))在動(dòng)作細(xì)化下是不保持的。一些工作研究了交織互模擬等價(jià)在嚴(yán)格限制動(dòng)作細(xì)化的情況下才能保持,但在這種限制下交織跡等價(jià)仍然不保持,沒有工作進(jìn)一步討
【學(xué)位授予單位】：中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2006
【分類號(hào)】：TP303

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 楊昕梅;孫秀莉;李紹榮;;基于動(dòng)作細(xì)化的握手?jǐn)U展[J];電子科技大學(xué)學(xué)報(bào);2011年03期

2 王煥寶;張佑生;;圖元的子句時(shí)新性[J];東南大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年S1期

3 韓婷婷;陳韜略;顏峰;呂建;;一個(gè)基于偏序事件結(jié)構(gòu)的Web服務(wù)模型及其形式化組裝[J];計(jì)算機(jī)科學(xué);2005年05期

4 張輝;于建江;湯克明;;用于整合SOA與EDA的智能化事件驅(qū)動(dòng)模型[J];計(jì)算機(jī)應(yīng)用研究;2009年09期

5 蔣昌俊;Petri網(wǎng)理論與方法研究綜述[J];控制與決策;1997年06期

6 趙錫英;;交互式馬爾可夫鏈代數(shù)的事件結(jié)構(gòu)模型[J];蘭州交通大學(xué)學(xué)報(bào);2008年03期

7 張曉東,柴躍廷,任守榘;一種形式化的構(gòu)件模型框架[J];清華大學(xué)學(xué)報(bào)(自然科學(xué)版);2000年03期

8 葉新銘,郝松俠;IPv6鄰居發(fā)現(xiàn)協(xié)議的形式化驗(yàn)證[J];軟件學(xué)報(bào);2005年06期

9 閆煒;吳盡昭;高新巖;;用基于流事件結(jié)構(gòu)的偏序時(shí)序邏輯刻畫并發(fā)系統(tǒng)多誘因特征[J];四川大學(xué)學(xué)報(bào)(工程科學(xué)版);2008年01期

10 徐克鵬;左春;;基于BPM的倉儲(chǔ)物流管理系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)系統(tǒng)應(yīng)用;2010年05期

相關(guān)博士學(xué)位論文 前9條

1 楊琛;打結(jié)不變的命題投影時(shí)序邏輯與模型檢測(cè)[D];西安電子科技大學(xué);2010年

2 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

3 張波;基于XML的分布式軟件體系結(jié)構(gòu)研究[D];中國科學(xué)院軟件研究所;2001年

4 任洪敏;基于π演算的軟件體系結(jié)構(gòu)形式化研究[D];復(fù)旦大學(xué);2003年

5 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測(cè)方法[D];中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

6 孫秀莉;基于動(dòng)作細(xì)化的異步電路自動(dòng)綜合[D];中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2005年

7 王海霞;運(yùn)算電路的形式化驗(yàn)證方法研究[D];中國科學(xué)院研究生院（計(jì)算技術(shù)研究所）;2004年

8 蔣昌俊;并發(fā)系統(tǒng)綜合的PN行為理論及其應(yīng)用[D];中國科學(xué)院研究生院（計(jì)算技術(shù)研究所）;1998年

9 鄭光;并發(fā)系統(tǒng)的動(dòng)作細(xì)化理論[D];蘭州大學(xué);2008年

相關(guān)碩士學(xué)位論文 前10條

1 張靜;基于SOA的電信綜合定單處理子系統(tǒng)的設(shè)計(jì)[D];河北科技大學(xué);2011年

2 王蜜;支持服務(wù)協(xié)同的PaaS平臺(tái)中服務(wù)動(dòng)態(tài)演化方法研究[D];山東大學(xué);2011年

3 許式陽;基于SOA的企業(yè)信息系統(tǒng)的研究與應(yīng)用[D];杭州電子科技大學(xué);2010年

4 李軍;軟構(gòu)件工程學(xué)習(xí)環(huán)境開發(fā)及應(yīng)用[D];大連理工大學(xué);2001年

5 趙云峰;低壓電力線信道建模及其仿真系統(tǒng)的研究[D];河海大學(xué);2003年

6 龍軍;關(guān)于密碼協(xié)議形式化驗(yàn)證方法的研究[D];國防科學(xué)技術(shù)大學(xué);2003年

7 曾瓊;概率進(jìn)程代數(shù)的度量指稱語義[D];中國科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

8 郭晉偉;SOA架構(gòu)的管理信息系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)院研究生院（沈陽計(jì)算技術(shù)研究所）;2006年

9 張之s，

本文編號(hào)：2699761