發(fā)布時(shí)間：2017-05-13 07:12

  本文關(guān)鍵詞：并發(fā)系統(tǒng)的建模與驗(yàn)證一體化方法的研究，由筆耕文化傳播整理發(fā)布。

【摘要】：現(xiàn)代軟硬件系統(tǒng)變得越來越復(fù)雜和智能化,并具有并發(fā)的特征。隨著并發(fā)系統(tǒng)的廣泛應(yīng)用,尤其在關(guān)系人們生命財(cái)產(chǎn)安全的領(lǐng)域,其可靠性受到高度重視。傳統(tǒng)的安全性保障方法主要基于測(cè)試技術(shù),難以保證測(cè)試用例覆蓋系統(tǒng)的所有可能執(zhí)行路徑。模型檢測(cè)通過數(shù)學(xué)方法驗(yàn)證系統(tǒng)模型是否滿足需求屬性,具有完備性和自動(dòng)化等優(yōu)點(diǎn),因而受到青睞。但是模型檢測(cè)的建模過程通常由手工完成,因此對(duì)于并發(fā)系統(tǒng),需要一種能夠描述其行為和功能的建模語言。設(shè)計(jì)和應(yīng)用針對(duì)并發(fā)系統(tǒng)的建模語言,其主要面臨的問題有:(1)如何描述系統(tǒng)的控制流和數(shù)據(jù)流以及并發(fā)等特征;(2)如何減少建模的成本,提高建模的效率;(3)如何保證系統(tǒng)、模型、驗(yàn)證之間的一致性;(4)如何解決系統(tǒng)的白箱驗(yàn)證與保密性之間的沖突。針對(duì)這些問題,本文做出以下研究工作:?提出針對(duì)并發(fā)系統(tǒng)的形式化建模語言MCD,并給出了其語法、語義和形式化定義。MCD使用模塊作為基本組件,定義層次事件自動(dòng)機(jī)和功能塊過程分別用于描述系統(tǒng)的控制流和數(shù)據(jù)流。層次事件自動(dòng)機(jī)通過狀態(tài)和變遷與功能塊過程統(tǒng)一起來。各個(gè)層次事件自動(dòng)機(jī)并發(fā)運(yùn)行,通過共享變量和信道進(jìn)行交互�；谛问交Z法和語義可以對(duì)系統(tǒng)模型進(jìn)行形式化驗(yàn)證和分析。?提出由MCD系統(tǒng)模型生成模型檢測(cè)代碼的算法。將層次事件自動(dòng)機(jī)翻譯生成線程,將功能塊過程翻譯生成內(nèi)聯(lián)函數(shù)。利用阻塞和隨機(jī)選擇機(jī)制實(shí)現(xiàn)模型的同步異步和不確定性。通過定義功能塊優(yōu)先級(jí)和端口變量解決數(shù)據(jù)流中帶環(huán)的部分。此外還可以根據(jù)用戶的需求和配置使用不同的優(yōu)化策略以減小系統(tǒng)的狀態(tài)空間和檢測(cè)時(shí)間。?基于MCD建模語言設(shè)計(jì)實(shí)現(xiàn)了模塊化建模與模型檢測(cè)一體化平臺(tái)M3C,該平臺(tái)沒有使用任何開源代碼和第三方庫,完全自主知識(shí)產(chǎn)權(quán)。M3C采用模塊和圖形化方式建模,自動(dòng)生成模型的檢測(cè)代碼并進(jìn)行模型檢測(cè),最后將檢測(cè)結(jié)果以可視化的方式顯示。還實(shí)現(xiàn)了語法檢查,模塊的自定義和復(fù)用等功能。M3C降低了形式化驗(yàn)證的使用門檻,同時(shí)提高了建模的正確性和效率。?使用M3C對(duì)列車通信網(wǎng)絡(luò)中的實(shí)際系統(tǒng)進(jìn)行了建模驗(yàn)證。經(jīng)過驗(yàn)證發(fā)現(xiàn)系統(tǒng)存在缺陷,可能導(dǎo)致功能異常。通過和系統(tǒng)設(shè)計(jì)人員溝通合作,找到并修復(fù)了錯(cuò)誤。證明了本文所提出的方法和工具的實(shí)用性。
【關(guān)鍵詞】：并發(fā)系統(tǒng) 模塊化建模 控制流 數(shù)據(jù)流 模型檢測(cè)
【學(xué)位授予單位】：清華大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP311.52
【目錄】：

• 摘要3-4
• Abstract4-7
• 第1章 緒論7-16
• 1.1 研究背景7-10
• 1.2 研究現(xiàn)狀10-13
• 1.3 論文貢獻(xiàn)13-15
• 1.4 論文結(jié)構(gòu)15-16
• 第2章 模塊化控制流與數(shù)據(jù)流建模語言16-43
• 2.1 引言16-17
• 2.2 MCD建模語言17-18
• 2.3 MCD建模語言的語法18-28
• 2.3.1 數(shù)據(jù)類型18-20
• 2.3.2 表達(dá)式20-21
• 2.3.3 層次事件自動(dòng)機(jī)21-24
• 2.3.4 功能塊過程24-28
• 2.3.5 MCD系統(tǒng)模型28
• 2.4 MCD建模語言的語義28-34
• 2.4.1 MCD系統(tǒng)模型28-29
• 2.4.2 層次事件自動(dòng)機(jī)29-31
• 2.4.3 功能塊過程31-34
• 2.5 MCD建模語言的形式化定義34-42
• 2.5.1 層次事件自動(dòng)機(jī)34-38
• 2.5.2 功能塊過程38-40
• 2.5.3 MCD系統(tǒng)模型40-41
• 2.5.4 形式化語義41-42
• 2.6 本章小結(jié)42-43
• 第3章 模型檢測(cè)代碼生成及優(yōu)化43-63
• 3.1 引言43-44
• 3.2 PROMELA44
• 3.3 數(shù)據(jù)類型與變量44-46
• 3.4 層次事件自動(dòng)機(jī)46-52
• 3.5 功能塊過程52-60
• 3.5.1 功能塊52-54
• 3.5.2 功能塊網(wǎng)絡(luò)54-60
• 3.6 MCD系統(tǒng)模型60-62
• 3.7 本章小結(jié)62-63
• 第4章 模塊化建模與模型檢測(cè)一體化平臺(tái)63-83
• 4.1 引言63
• 4.2 整體設(shè)計(jì)63-68
• 4.3 建模工具68-75
• 4.3.1 數(shù)據(jù)類型和變量69-70
• 4.3.2 控制流和數(shù)據(jù)流70-73
• 4.3.3 布線73-75
• 4.3.4 需求屬性75
• 4.4 翻譯優(yōu)化工具75-77
• 4.5 驗(yàn)證分析工具77-80
• 4.6 輔助工具80-82
• 4.7 本章小結(jié)82-83
• 第5章 應(yīng)用案例83-100
• 5.1 引言83
• 5.2 MVB83-89
• 5.3 WTB89-99
• 5.4 本章小結(jié)99-100
• 第6章 結(jié)束語100-103
• 6.1 工作總結(jié)100-101
• 6.2 研究展望101-103
• 參考文獻(xiàn)103-108
• 致謝108-110
• 個(gè)人簡(jiǎn)歷、在學(xué)期間發(fā)表的學(xué)術(shù)論文與研究成果110-111

【相似文獻(xiàn)】

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

1 王詠剛;;并發(fā)系統(tǒng)的測(cè)試[J];程序員;2004年03期

2 齊微;李青山;陳平;趙蕓;杜寬利;;多機(jī)并發(fā)系統(tǒng)動(dòng)態(tài)信息的逆向抽取和過濾策略[J];系統(tǒng)工程與電子技術(shù);2006年09期

3 王金雙;張興元;楊華兵;張毓森;;并發(fā)系統(tǒng)概率空間的形式化構(gòu)造方法[J];計(jì)算機(jī)工程與科學(xué);2008年11期

4 付立軍;;醫(yī)院實(shí)時(shí)多并發(fā)系統(tǒng)的研究[J];價(jià)值工程;2011年09期

5 馮玉琳,趙旭東,郭端陽;并發(fā)系統(tǒng)的模型和自動(dòng)驗(yàn)證[J];計(jì)算機(jī)學(xué)報(bào);1990年02期

6 劉建福,徐德啟;并發(fā)系統(tǒng)的模型與驗(yàn)證[J];蘭州大學(xué)學(xué)報(bào);1992年01期

7 張廣泉,戎玫,沈一棟;并發(fā)系統(tǒng)基本模型及其分析[J];重慶大學(xué)學(xué)報(bào)(自然科學(xué)版);1998年03期

8 劉劍,李彤;一種并發(fā)系統(tǒng)的規(guī)約方法[J];計(jì)算機(jī)應(yīng)用研究;2000年05期

9 李楊;程建華;房鼎益;陳曉江;馮健;;并發(fā)系統(tǒng)的安全性與活性的驗(yàn)證方法[J];計(jì)算機(jī)工程與應(yīng)用;2008年04期

10 魚先鋒;王輝;;并發(fā)系統(tǒng)互斥約束的形式化驗(yàn)證[J];商洛學(xué)院學(xué)報(bào);2011年06期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫 前4條

1 燕飛;唐濤;;實(shí)時(shí)并發(fā)系統(tǒng)的形式化建模方法研究[A];2009系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2009年

2 陳曉江;楊琛;馮健;房鼎益;;并發(fā)系統(tǒng)模型檢測(cè)中的狀態(tài)約減算法[A];2007年全國(guó)開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊(cè))[C];2007年

3 蔣昌俊;疏松桂;鄭應(yīng)平;;隨機(jī)Petri網(wǎng)同步并發(fā)行為的量化分析[A];1994中國(guó)控制與決策學(xué)術(shù)年會(huì)論文集[C];1994年

4 朱連章;魏曉慧;;基于著色Petri網(wǎng)避免并發(fā)系統(tǒng)死鎖的方法[A];2008通信理論與技術(shù)新進(jìn)展——第十三屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集（上）[C];2008年

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

1 夏默;并發(fā)系統(tǒng)的建模與驗(yàn)證一體化方法的研究[D];清華大學(xué);2015年

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

3 吳鵬;并發(fā)系統(tǒng)的模型檢測(cè)與測(cè)試[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2005年

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

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

1 王婷;基于偏序簡(jiǎn)化的并發(fā)系統(tǒng)模型檢測(cè)技術(shù)的研究[D];西北大學(xué);2007年

2 賀彥琨;并發(fā)系統(tǒng)的事件結(jié)構(gòu)模型初步研究[D];蘭州大學(xué);2008年

3 楊琛;基于進(jìn)程代數(shù)并發(fā)系統(tǒng)的建模與驗(yàn)證研究[D];西北大學(xué);2006年

4 宋琳;概率進(jìn)程演算的互模擬分析[D];上海交通大學(xué);2007年

5 申慧;并發(fā)系統(tǒng)的并行計(jì)算及性能分析[D];浙江理工大學(xué);2011年

6 宋磊;概率符號(hào)Pi演算的有限公理化[D];上海交通大學(xué);2009年

  本文關(guān)鍵詞：并發(fā)系統(tǒng)的建模與驗(yàn)證一體化方法的研究，，由筆耕文化傳播整理發(fā)布。

本文編號(hào)：361878