本文關(guān)鍵詞：面向邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)的進(jìn)程演算CLL_R的研究

  更多相關(guān)文章： 形式化方法 并發(fā)系統(tǒng) 混合規(guī)范 邏輯標(biāo)記轉(zhuǎn)換系統(tǒng) 進(jìn)程演算 計(jì)算樹邏輯 公理化

【摘要】：為了形式化規(guī)范、驗(yàn)證和分析反應(yīng)式并發(fā)系統(tǒng),學(xué)術(shù)界提出并發(fā)展了多種形式化規(guī)范方法。這些方法大體上可分為兩類：基于動作的和基于狀態(tài)的�；趧幼鞯囊�(guī)范方法以進(jìn)程代數(shù)(演算)最具代表性；基于狀態(tài)的方法通常以模態(tài)邏輯或μ-演算描述系統(tǒng)規(guī)范。這兩類方法基于不同的觀點(diǎn),對形式規(guī)范和驗(yàn)證進(jìn)行了深入而廣泛的研究,具有互補(bǔ)的優(yōu)點(diǎn)：前者支持規(guī)范的組合式(compositional)構(gòu)造、分析和推理；后者擅長描述系統(tǒng)整體和抽象性質(zhì)。十余年來,學(xué)術(shù)界期望構(gòu)建一種允許上述兩種不同風(fēng)格規(guī)范并存且混合使用的架構(gòu),以此實(shí)現(xiàn)可以同時利用它們各自長處的目的。在此愿景驅(qū)使下,多種所謂混合規(guī)范方法被相繼提出,其中,Luttgen和’Vogler近年提出的邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)(簡記為LLTS)克服了其它方法的缺陷,是一個允許自由混合使用通常進(jìn)程算子和邏輯算子進(jìn)行規(guī)范的語義框架。本文旨在基于純演算的方法針對LITS在理論研究上的空白和缺陷開展工作,主要工作包括如下方面：(1)構(gòu)建面向LLTS的進(jìn)程演算系統(tǒng)CLLR該工作不但將Luttgen和’Vogle r的工作(不含隱藏算子)提升到純演算的風(fēng)格,更主要的貢獻(xiàn)在于深入研究了他們沒有涉及的遞歸算子。在深入研究環(huán)境(context)遞歸進(jìn)程的展開與進(jìn)程轉(zhuǎn)換之間的內(nèi)在聯(lián)系基礎(chǔ)上,我們較為系統(tǒng)地發(fā)展了CLLR的行為理論,證明了Luttgen和’Vogler提出的預(yù)備模擬關(guān)系相對CLLR所有算子的前同余性(preoongruence)從而在理論上保證了CLLR可以支持規(guī)范組合式的構(gòu)造、分析和推理。作為面向LLTS的演算系統(tǒng)CLLR包含了邏輯合取和析取算子,并需要處理邏輯復(fù)合所帶來的進(jìn)程協(xié)調(diào)性問題。正因?yàn)檫M(jìn)程協(xié)調(diào)性對進(jìn)程行為的發(fā)散所具有的敏感性,使得CLLR中的遞歸算子處理較之通常進(jìn)程演算要相對困難和復(fù)雜許多。(2)在充分考慮協(xié)調(diào)進(jìn)程與非協(xié)調(diào)進(jìn)程行為差異的基礎(chǔ)上,提出了CLLR的公理系統(tǒng)AXCLL,并證明了該系統(tǒng)的可靠性以及相對無遞歸進(jìn)程的基完備性,從而揭示了通常進(jìn)程算子與邏輯合取及析取算子在預(yù)備模擬關(guān)系下所遵循的代數(shù)律。(3)研究了CLLR中形如X=RStx方程的解,證明了唯一解定理和最大解定理。前者給出了這類方程存在唯一解的充分條件；后者揭示了遞歸進(jìn)程X X=tx與X=Rs tx的解之間的內(nèi)在聯(lián)系：若X是tx的強(qiáng)有衛(wèi)變元,則X X=tx是滿足等式X=RStx的最“粗糙”的規(guī)范。(4)作為遞歸算子與方程最大解定理的應(yīng)用,我們研究了將基于動作的計(jì)算樹邏輯ACTL表示安全性質(zhì)的語言片段在CLLR中進(jìn)行編碼的問題。該研究在理論上保證了CLLR具有描述安全性質(zhì)的表達(dá)能力,同時將判定進(jìn)程是否滿足(表示安全性的)ACTL公式的模型檢測問題歸約為判定進(jìn)程之間是否具有精化關(guān)系的驗(yàn)證問題。由于遞歸算子的使用,該工作所提供的編碼極大簡化了Luttgen和、Voler的原有編碼�？傊�,上述研究將LLTS框架上原有的工作演算化(未包括隱藏算子),在此基礎(chǔ)上較深入研究了LUttgen和’Vogler原有工作中沒有涉及的若干重要的理論問題,包括：遞歸算子及其行為理論、方程解以及公理化等,并且本文在ACTL公式編碼方面的工作極大簡化了他們原有處理方式。與通常進(jìn)程演算系統(tǒng)比較CLLR的特點(diǎn)在于考慮了進(jìn)程的邏輯復(fù)合以及邏輯復(fù)合所帶來的協(xié)調(diào)性問題,允許自由地混合使用通常的進(jìn)程操作算子、遞歸算子、邏輯合取和析取算子以及模態(tài)詞unless和unless(weak until)進(jìn)行規(guī)范描述,并且支持規(guī)范組合式構(gòu)造、推理和分析。
【關(guān)鍵詞】：形式化方法 并發(fā)系統(tǒng) 混合規(guī)范 邏輯標(biāo)記轉(zhuǎn)換系統(tǒng) 進(jìn)程演算 計(jì)算樹邏輯 公理化
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP301
【目錄】：

• 摘要4-6
• ABSTRACT6-12
• 第一章 緒論12-20
• 1.1 反應(yīng)式并發(fā)系統(tǒng)及其形式化規(guī)范12-14
• 1.2 混合規(guī)范14-15
• 1.3 邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)15-17
• 1.4 本文的主要工作17-18
• 1.5 本文的內(nèi)容安排18-20
• 第二章 預(yù)備知識20-26
• 2.1 記號約定20
• 2.2 邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)與預(yù)備模擬關(guān)系20-23
• 2.3 轉(zhuǎn)換系統(tǒng)規(guī)范理論23-26
• 第三章 CLL_R及其操作語義26-40
• 3.1 CLL_R的語法及結(jié)構(gòu)化操作語義規(guī)則26-29
• 3.2 CLL_R的穩(wěn)固模型與標(biāo)記轉(zhuǎn)換系統(tǒng)29-31
• 3.3 CLL_R轉(zhuǎn)換模型的基本性質(zhì)31-38
• 3.4 本章小結(jié)38-40
• 第四章 展開、環(huán)境與轉(zhuǎn)換40-58
• 4.1 展開及其基本性質(zhì)40-42
• 4.2 環(huán)境與單步轉(zhuǎn)換42-50
• 4.3 τ轉(zhuǎn)換序列和典范路徑50-57
• 4.4 本章小結(jié)57-58
• 第五章 CLL_R的前同余性58-78
• 5.1 若干引理58-71
• 5.2 (?)RS的前同余性71-76
• 5.3 本章小結(jié)76-78
• 第六章 CLL_R的公理系統(tǒng)78-96
• 6.1 公理系統(tǒng)AX_(CLL)78-81
• 6.2 AX_(CLL)的可靠性81-86
• 6.3 范式定理與基完備性86-94
• 6.4 本章小結(jié)94-96
• 第七章 CLL_R中一類方程的解96-112
• 7.1 唯一解定理96-105
• 7.2 最大解定理105-110
• 7.3 本章小結(jié)110-112
• 第八章 CLL_R與基于動作的計(jì)算樹邏輯112-126
• 8.1 基于動作的計(jì)算樹邏輯的一個片段在CLL_R中的編碼112-113
• 8.2 編碼的正確性113-121
• 8.3 例子121-124
• 8.4 本章小結(jié)124-126
• 第九章 總結(jié)與展望126-128
• 參考文獻(xiàn)128-138
• 致謝138-140
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文140

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 段國旺;畢秋閣;張風(fēng)光;張洪峰;;溫度多路轉(zhuǎn)換系統(tǒng)在延遲焦化加熱爐改造中的應(yīng)用[J];科技信息;2012年31期

2 左渝斌,馮生榮;一種光學(xué)轉(zhuǎn)換系統(tǒng)的實(shí)際應(yīng)用[J];紅外技術(shù);2001年01期

3 張帥;賈珈;楊大利;徐明星;蔡蓮紅;;方言轉(zhuǎn)換系統(tǒng)中的音節(jié)切分算法研究[J];計(jì)算機(jī)技術(shù)與發(fā)展;2009年07期

4 董子剛;李嚴(yán);張?jiān)?;一種新的模擬到信息轉(zhuǎn)換系統(tǒng)[J];電子學(xué)報(bào);2013年09期

5 錢玉趾 ,楊永玲;轉(zhuǎn)換系統(tǒng)——一個美麗的夢[J];中文信息;1994年02期

6 伍劍;;自動語音轉(zhuǎn)換系統(tǒng)[J];金色少年;2009年03期

7 朱澤彬,黃會群,何锫;轉(zhuǎn)換系統(tǒng)的設(shè)計(jì)及其應(yīng)用[J];長沙理工大學(xué)學(xué)報(bào)(自然科學(xué)版);2005年03期

8 沈達(dá)陽;孫茂松;;漢字簡繁體智能化轉(zhuǎn)換系統(tǒng)[J];中文信息;1996年06期

9 張孝存;字本位和語本位——談鍵盤輸入和“轉(zhuǎn)換系統(tǒng)”[J];中文信息;1996年05期

10 何銘;嚴(yán)克勤;;自動化播出的又一新課題——節(jié)目串聯(lián)單管理與轉(zhuǎn)換系統(tǒng)[J];電視工程;2000年02期

中國重要會議論文全文數(shù)據(jù)庫 前1條

1 張運(yùn)森;劉保國;劉珂;;STEP與XML轉(zhuǎn)換系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)[A];全國先進(jìn)制造技術(shù)高層論壇暨第八屆制造業(yè)自動化與信息化技術(shù)研討會論文集[C];2009年

中國重要報(bào)紙全文數(shù)據(jù)庫 前2條

1 教育部語信司;“簡繁漢字智能轉(zhuǎn)換系統(tǒng)”通過結(jié)項(xiàng)鑒定[N];語言文字周報(bào);2014年

2 記者 萬玉鳳;《漢字簡繁文本智能轉(zhuǎn)換系統(tǒng)》發(fā)布[N];中國教育報(bào);2014年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前3條

1 張嚴(yán);面向邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)的進(jìn)程演算CLL_R的研究[D];南京航空航天大學(xué);2015年

2 張晉津;轉(zhuǎn)換系統(tǒng)行為近似等價性的研究[D];南京航空航天大學(xué);2010年

3 蔣澤甫;風(fēng)電轉(zhuǎn)換系統(tǒng)可靠性評估及其薄弱環(huán)節(jié)辨識[D];重慶大學(xué);2012年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前8條

1 戴健文;面向真實(shí)感渲染的材質(zhì)轉(zhuǎn)換系統(tǒng)與優(yōu)化[D];浙江大學(xué);2016年

2 周瑩;高質(zhì)量語音轉(zhuǎn)換系統(tǒng)中關(guān)鍵技術(shù)的研究[D];南京郵電大學(xué);2012年

3 李淑卿;移動數(shù)據(jù)實(shí)時轉(zhuǎn)換系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];北京郵電大學(xué);2008年

4 張宇奇;基于FPGA的信息交聯(lián)轉(zhuǎn)換系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];西安電子科技大學(xué);2014年

5 陳志鋒;通信協(xié)議轉(zhuǎn)換系統(tǒng)的實(shí)現(xiàn)[D];蘇州大學(xué);2005年

6 范忠鋒;Ada83/95轉(zhuǎn)換系統(tǒng)——后端設(shè)計(jì)與實(shí)現(xiàn)[D];西安電子科技大學(xué);2002年

7 鄭麒;Ada83/95轉(zhuǎn)換系統(tǒng)前端的研究與實(shí)現(xiàn)[D];西安電子科技大學(xué);2002年

8 童波;特定對象漢語語音轉(zhuǎn)換系統(tǒng)的研究[D];華北電力大學(xué)（北京）;2010年

，

本文編號：1028426