本文關(guān)鍵詞：擴(kuò)展π演算的建模、驗(yàn)證與測試，由筆耕文化傳播整理發(fā)布。

【摘要】：時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)是以并發(fā)性、移動(dòng)性、時(shí)間相關(guān)性和異構(gòu)性等為主要特征的計(jì)算系統(tǒng)。對于這類系統(tǒng),特別是安全攸關(guān)的時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng),如移動(dòng)支付系統(tǒng)、移動(dòng)通信系統(tǒng)、交通控制系統(tǒng)等,其失誤和崩潰可能會(huì)造成重大損失,因此時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的正確性、安全性等質(zhì)量屬性受到人們的普遍重視。對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)采用以嚴(yán)格數(shù)學(xué)理論為支撐的形式化方法進(jìn)行建模、驗(yàn)證與測試是行之有效的減少系統(tǒng)設(shè)計(jì)錯(cuò)誤和保證系統(tǒng)質(zhì)量的重要途徑。進(jìn)程代數(shù),作為形式化方法的代表,是一種重要的用于對并發(fā)系統(tǒng)進(jìn)行建模和驗(yàn)證的技術(shù)。由于所面向的領(lǐng)域和應(yīng)用背景的不同,涌現(xiàn)出很多進(jìn)程代數(shù)的分支和變種,其中演算就是用于建模移動(dòng)性的重要的分支。近年來,由于新型網(wǎng)絡(luò)技術(shù)和信息技術(shù)的不斷發(fā)展,使得能夠建模和驗(yàn)證移動(dòng)系統(tǒng)的演算得到人們的廣泛關(guān)注。但是,演算在對系統(tǒng)建模時(shí)并未考慮到動(dòng)作執(zhí)行所占用的時(shí)間以及系統(tǒng)在某個(gè)狀態(tài)所持續(xù)的時(shí)間,故而,使得它不適于對時(shí)間相關(guān)系統(tǒng)進(jìn)行建模、驗(yàn)證和測試。為了對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和驗(yàn)證,本文研究了添加時(shí)間相關(guān)特性的擴(kuò)展的演算。在此基礎(chǔ)上,提出采用擴(kuò)展演算為時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和推演的方法。進(jìn)一步地,為了對擴(kuò)展演算建模的系統(tǒng)進(jìn)行自動(dòng)驗(yàn)證,提出將擴(kuò)展演算轉(zhuǎn)換為建模、仿真驗(yàn)證語言MSVL的方法。此外,為了對擴(kuò)展演算建模的系統(tǒng)進(jìn)行測試,文章還給出了采用擴(kuò)展演算的測試用例生成方法。所取得的研究成果主要有以下幾個(gè)方面。(1)建立了帶區(qū)間動(dòng)作前綴的擴(kuò)展演算p-π,定義了p-π的語法和操作語義,給出了p-π的代數(shù)性質(zhì)和時(shí)間相關(guān)性質(zhì)并對其進(jìn)行了證明。在此基礎(chǔ)上給出了p-π對時(shí)間相關(guān)行為的建模。此外,還通過實(shí)例對p-π的應(yīng)用效果和相應(yīng)性質(zhì)所起的作用進(jìn)行了分析和說明。(2)提出了采用擴(kuò)展演算對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和推演的方法。采用區(qū)間動(dòng)作前綴和瞬時(shí)動(dòng)作前綴分別描述系統(tǒng)的時(shí)間相關(guān)行為和交互行為,并通過操作算子將子進(jìn)程進(jìn)行復(fù)合,然后利用操作規(guī)則構(gòu)造出系統(tǒng)的時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)和可接受的執(zhí)行路徑,基于上述遷移系統(tǒng)和執(zhí)行路徑完成對系統(tǒng)性質(zhì)的推演。通過移動(dòng)車輛控制系統(tǒng)的分析表明,所提方法可對時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行有效建模和推演,保證時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的可靠性。(3)提出了從擴(kuò)展演算p-π到MSVL的轉(zhuǎn)換方法。為了完成轉(zhuǎn)換,先在MSVL中對通道和通信原語進(jìn)行了定義�；谠摱x,給出了從p-π到MSVL的結(jié)構(gòu)化轉(zhuǎn)換規(guī)則,并對二者采用的通信機(jī)制間存在的一致性進(jìn)行了證明。為了說明轉(zhuǎn)換的合理性,文章還證明在p-π進(jìn)程和MSVL的格局間存在互模擬關(guān)系。這樣,通過轉(zhuǎn)換,就可以借助MSVL建模仿真驗(yàn)證工具完成對p-π進(jìn)程的驗(yàn)證。(4)提出了基于擴(kuò)展演算的測試用例生成方法。采用p-π為時(shí)間相關(guān)并發(fā)系統(tǒng)建模并由p-π的操作規(guī)則構(gòu)造出系統(tǒng)模型的時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)。基于時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)和用例規(guī)約生成測試用例,測試用例的生成滿足執(zhí)行動(dòng)作覆蓋準(zhǔn)則、路徑覆蓋準(zhǔn)則和時(shí)間約束覆蓋準(zhǔn)則,并給出了測試用例的選擇策略。同時(shí)通過p-π的驗(yàn)證方法,還保證了所產(chǎn)生的測試用例的正確性。
【關(guān)鍵詞】：進(jìn)程代數(shù) π演算 規(guī)范 形式驗(yàn)證 基于模型的測試
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP301
【目錄】：

• 摘要5-7
• ABSTRACT7-11
• 縮略詞對照表11-17
• 第一章 緒論17-31
• 1.1 研究背景與意義17-18
• 1.2 形式化模型18-21
• 1.2.1 基于圖形化的模型18-19
• 1.2.2 基于文本的模型19-21
• 1.3 形式化驗(yàn)證21-23
• 1.3.1 模型檢測21-22
• 1.3.2 定理證明22-23
• 1.4 基于模型的測試23-25
• 1.4.1 基于非形式化模型的測試24
• 1.4.2 基于形式化模型的測試24-25
• 1.5 相關(guān)研究工作與本文研究目的25-28
• 1.5.1 相關(guān)研究工作25-28
• 1.5.2 本文研究目的28
• 1.6 論文的主要工作與組織結(jié)構(gòu)28-31
• 第二章 π演算與MSVL31-45
• 2.1 π演算31-35
• 2.1.1 π演算的語法和語義31-33
• 2.1.2 π演算的移動(dòng)性33-34
• 2.1.3 π演算的研究進(jìn)展34-35
• 2.2 建模、仿真與驗(yàn)證語言MSVL35-44
• 2.2.1 投影時(shí)序邏輯PTL35-38
• 2.2.2 MSVL38-44
• 2.3 本章小結(jié)44-45
• 第三章 擴(kuò)展π演算 p-π45-65
• 3.1 p-π的語法45-46
• 3.2 p-π的語義46-50
• 3.2.1 結(jié)構(gòu)等價(jià)46-47
• 3.2.2 操作規(guī)則47-50
• 3.3 p-π的性質(zhì)50-56
• 3.3.1 代數(shù)性質(zhì)50-55
• 3.3.2 時(shí)間相關(guān)性質(zhì)55-56
• 3.4 時(shí)間相關(guān)行為的建模56-58
• 3.4.1 時(shí)間延遲56-57
• 3.4.2 超時(shí)處理57
• 3.4.3 中斷處理57-58
• 3.5 實(shí)例58-63
• 3.6 本章小結(jié)63-65
• 第四章 時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的建模與推演65-75
• 4.1 系統(tǒng)描述65-67
• 4.2 系統(tǒng)建模67-71
• 4.3 系統(tǒng)推演71-73
• 4.3.1 基于操作規(guī)則的系統(tǒng)遷移71-72
• 4.3.2 基于系統(tǒng)遷移的系統(tǒng)推演72-73
• 4.4 本章小結(jié)73-75
• 第五章 從p-π到MSVL的結(jié)構(gòu)化轉(zhuǎn)換方法75-95
• 5.1 MSVL的通道和通信原語76-77
• 5.2 從p-π到MSVL的轉(zhuǎn)換77-87
• 5.2.1 名字和原子命題的轉(zhuǎn)換78
• 5.2.2 進(jìn)程的轉(zhuǎn)換78-84
• 5.2.3 Interleaving和True Concurrency間的一致性84-86
• 5.2.4 注意86-87
• 5.3 轉(zhuǎn)換的合理性87-90
• 5.4 應(yīng)用實(shí)例90-94
• 5.4.1 系統(tǒng)建模90-91
• 5.4.2 轉(zhuǎn)換91-92
• 5.4.3 驗(yàn)證92-94
• 5.5 本章小結(jié)94-95
• 第六章 采用擴(kuò)展π演算的測試用例生成方法95-109
• 6.1 時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)96-97
• 6.2 測試用例生成97-103
• 6.2.1 執(zhí)行路徑97-99
• 6.2.2 可觀察動(dòng)作與不可觀察動(dòng)作99
• 6.2.3 覆蓋準(zhǔn)則99
• 6.2.4 互模擬進(jìn)程替換99-100
• 6.2.5 基于對象約束語言的用例規(guī)約100
• 6.2.6 測試用例生成算法100-101
• 6.2.7 測試用例選擇策略101-103
• 6.3 應(yīng)用實(shí)例103-107
• 6.3.1 OBS的p-π系統(tǒng)進(jìn)程103-104
• 6.3.2 系統(tǒng)的TDLTS104-105
• 6.3.3 測試用例生成105-107
• 6.4 相關(guān)方法比較107
• 6.5 本章小結(jié)107-109
• 第七章 總結(jié)與展望109-113
• 7.1 全文總結(jié)109-110
• 7.2 未來的研究工作110-113
• 附錄A113-115
• 參考文獻(xiàn)115-125
• 致謝125-127
• 作者簡介127-128
• 1. 基本情況127
• 2. 教育背景127
• 3. 攻讀博士學(xué)位期間的研究成果127-128

【相似文獻(xiàn)】

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

1 路曉麗;葛瑋;陳新麗;郝克剛;;支持共享和復(fù)用的測試用例庫系統(tǒng)的設(shè)計(jì)[J];計(jì)算機(jī)科學(xué);2006年05期

2 胡珊;楊豐玉;張曄;劉琳嵐;;基于測試項(xiàng)抽取的測試用例復(fù)用方法[J];微電子學(xué)與計(jì)算機(jī);2010年01期

3 張德平;查日軍;;劃分測試用例選擇的風(fēng)險(xiǎn)決策方法[J];計(jì)算機(jī)應(yīng)用研究;2010年12期

4 楊翊;陳挺;許崢;;證券軟件的測試用例設(shè)計(jì)充分性實(shí)踐[J];中國證券期貨;2012年07期

5 張智軼;陳振宇;徐寶文;楊瑞;;測試用例演化研究進(jìn)展[J];軟件學(xué)報(bào);2013年04期

6 楊悅;秦湘河;楊永安;郭榮;;航天測控軟件測試用例標(biāo)準(zhǔn)及應(yīng)用研究[J];無線電工程;2013年09期

7 王侃,盧慶齡,彭艷麗;測試用例自動(dòng)生成的鏈方法研究與實(shí)現(xiàn)[J];裝甲兵工程學(xué)院學(xué)報(bào);2001年03期

8 李順華;測試用例管理方法探討[J];飛航導(dǎo)彈;2001年05期

9 徐仁佐,陳斌,陳波,吳閩泉,熊忠偉;構(gòu)造面向?qū)ο筌浖蓮?fù)用測試用例的模式研究[J];武漢大學(xué)學(xué)報(bào)(理學(xué)版);2003年05期

10 陳紹英;金成姬;;性能測試用例[J];程序員;2004年11期

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

1 王道堂;林春哲;張凱;;軟件測試用例構(gòu)造方法與手段[A];計(jì)算機(jī)技術(shù)在工程建設(shè)中的應(yīng)用——第十二屆全國工程建設(shè)計(jì)算機(jī)應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2004年

2 李磊;曹先彬;;基于進(jìn)化的軟件測試用例生成方法[A];2005年“數(shù)字安徽”博士科技論壇論文集[C];2005年

3 徐李勤;王潔寧;;基于層次有色Petri網(wǎng)的軟件測試用例選取研究[A];全國第二屆信號處理與應(yīng)用學(xué)術(shù)會(huì)議�？痆C];2008年

4 林春哲;張凱;王道堂;;軟件測試用例設(shè)計(jì)分析[A];計(jì)算機(jī)技術(shù)在工程建設(shè)中的應(yīng)用——第十二屆全國工程建設(shè)計(jì)算機(jī)應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2004年

5 張俠影;李志蜀;;一種優(yōu)化的測試用例約簡方法[A];2008'中國信息技術(shù)與應(yīng)用學(xué)術(shù)論壇論文集（一）[C];2008年

6 張德平;聶長海;徐寶文;;劃分測試用例選擇策略研究[A];第五屆中國測試學(xué)術(shù)會(huì)議論文集[C];2008年

7 郭從穎;;場景驅(qū)動(dòng)測試用例設(shè)計(jì)及其測試自動(dòng)化技術(shù)研究[A];中國計(jì)量協(xié)會(huì)冶金分會(huì)2008年會(huì)論文集[C];2008年

8 郭從穎;;場景驅(qū)動(dòng)測試用例設(shè)計(jì)及其測試自動(dòng)化技術(shù)研究[A];2008全國第十三屆自動(dòng)化應(yīng)用技術(shù)學(xué)術(shù)交流會(huì)論文集[C];2008年

9 周曉燕;李兵;潘偉豐;覃葉宜;;基于錯(cuò)誤傳播概率網(wǎng)絡(luò)的軟件回歸測試用例選擇[A];第五屆全國復(fù)雜網(wǎng)絡(luò)學(xué)術(shù)會(huì)議論文（摘要）匯集[C];2009年

10 萬琳;張威;馬雪雁;陳曼青;;基于路徑的測試用例自動(dòng)生成技術(shù)[A];第十屆全國容錯(cuò)計(jì)算學(xué)術(shù)會(huì)議論文集[C];2003年

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

1 深圳市信息無障礙研究會(huì) 戴杰;“聽”軟件的IT工程師[N];人民政協(xié)報(bào);2014年

2 謝敏 沈雪芳 戴金龍;解決軟件測試的近憂和遠(yuǎn)慮[N];計(jì)算機(jī)世界;2005年

3 計(jì)算機(jī)世界實(shí)驗(yàn)室 韓勖;撥云見日[N];計(jì)算機(jī)世界;2008年

4 《網(wǎng)絡(luò)世界》記者 鄭楠;ONF測試步伐有條不紊[N];網(wǎng)絡(luò)世界;2014年

5 ;找錯(cuò)[N];計(jì)算機(jī)世界;2002年

6 信息產(chǎn)業(yè)部軟件與集成電路促進(jìn)中心 于明邋唐仕武;駛?cè)霚y試“快車道”[N];計(jì)算機(jī)世界;2007年

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

1 羅玲;擴(kuò)展π演算的建模、驗(yàn)證與測試[D];西安電子科技大學(xué);2015年

2 李麗;航天相機(jī)主控軟件測試用例自動(dòng)生成技術(shù)的研究[D];中國科學(xué)院研究生院（長春光學(xué)精密機(jī)械與物理研究所）;2010年

3 黃如兵;組合測試用例的自適應(yīng)隨機(jī)生成與優(yōu)先級排序方法研究[D];華中科技大學(xué);2013年

4 張娟;軟件測試中測試用例復(fù)用的研究[D];上海大學(xué);2012年

5 游亮;回歸測試用例選擇技術(shù)研究[D];華中科技大學(xué);2012年

6 謝曉東;基于模型比較的軟件測試用例生成方法研究[D];華中科技大學(xué);2007年

7 李根;基于動(dòng)態(tài)測試用例生成的二進(jìn)制軟件缺陷自動(dòng)發(fā)掘技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2010年

8 邢穎;測試用例自動(dòng)生成的分支限界算法及實(shí)驗(yàn)研究[D];北京郵電大學(xué);2014年

9 錢思佑;圖形用戶界面測試中相關(guān)問題研究[D];中國科學(xué)技術(shù)大學(xué);2010年

10 李軍義;軟件測試用例自動(dòng)生成技術(shù)研究[D];湖南大學(xué);2008年

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

1 田春艷;基于灰色關(guān)聯(lián)逼近理想解方法的測試用例評價(jià)模型研究[D];昆明理工大學(xué);2009年

2 唐海鵬;基于Additional策略回歸測試用例優(yōu)先級排序優(yōu)化研究[D];西南大學(xué);2015年

3 陳夢云;基于圈復(fù)雜度和調(diào)用次數(shù)的測試用例排序方法[D];上海師范大學(xué);2015年

4 姚瑞超;廣東電網(wǎng)測試用例自動(dòng)生成工具的研究與設(shè)計(jì)[D];華南理工大學(xué);2015年

5 張澤林;基于數(shù)據(jù)挖掘的軟件多故障定位與分析技術(shù)[D];南京理工大學(xué);2015年

6 鄒炳松;嵌入式軟件的圖形化測試用例生成系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)[D];哈爾濱工業(yè)大學(xué);2015年

7 李錦程;基于微信平臺(tái)的醫(yī)療就診系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)[D];哈爾濱工業(yè)大學(xué);2015年

8 趙群;軟件錯(cuò)誤定位中的巧合正確性問題研究[D];哈爾濱工業(yè)大學(xué);2015年

9 常龍輝;Web應(yīng)用的測試用例優(yōu)化生成與優(yōu)先級技術(shù)[D];上海大學(xué);2015年

10 王令賽;基于粒子群優(yōu)化算法的測試用例生成技術(shù)研究[D];中國礦業(yè)大學(xué);2015年

  本文關(guān)鍵詞：擴(kuò)展π演算的建模、驗(yàn)證與測試，，由筆耕文化傳播整理發(fā)布。

本文編號：342669