發(fā)布時間：2021-06-11 06:57

　　隨著計算機軟硬件體系的發(fā)展,能夠確保其安全、可靠的形式化驗證成為研究熱點。其中,模型檢測作為一種用來驗證有限狀態(tài)系統(tǒng)是否滿足形式化規(guī)范的高度自動化的驗證方法,備受關(guān)注。但是隨著形式化方法的發(fā)展,約束規(guī)則的增加以及狀態(tài)空間的復雜,如何更好地提高大規(guī)模約束規(guī)則查詢的速度,保證具有復雜狀態(tài)的模型檢測的效率,已經(jīng)成為一個迫切需要得到解決的問題。在形式規(guī)約方面,面對大規(guī)模約束查詢,基于單節(jié)點的約束查詢方法已經(jīng)無法高效地完成大規(guī)模的查詢?nèi)蝿?wù),例如對象約束語言的約束查詢效率過低問題。在形式驗證方面,面對復雜系統(tǒng)模型檢測,可能導致狀態(tài)爆炸問題,例如計算樹邏輯模型檢測狀態(tài)爆炸問題。相關(guān)研究表明可以利用云計算平臺,解決上述形式化方法面臨的問題,保證相關(guān)查詢以及驗證算法的效率。在此基礎(chǔ)上,本文為了應(yīng)對大量約束查詢帶來的挑戰(zhàn),提高OCL查詢的速度,提出了一種基于MapReduce的OCL并行查詢方法。這種方法通過提取OCL對象屬性集合,實現(xiàn)從OCL規(guī)則庫查詢到OCL對象屬性查詢的轉(zhuǎn)化,并利用MapReduce實現(xiàn)對象屬性并行查詢,縮短了OCL查詢時間。實驗結(jié)果表明,利用MapReduce實現(xiàn)對象屬性并行查詢,... 

【文章來源】：南京郵電大學江蘇省

【文章頁數(shù)】：66 頁

【學位級別】：碩士

【部分圖文】：

XML文檔片段其中第一個和中間的部分是一個對象屬性，在該片段中表示一個Owner(車主對象)

圖 3.5 Owner 特征集合CL 并行查詢處理CL 并行查詢輸入的數(shù)據(jù)實際上是 OCL 對象屬性集合。根據(jù)上一小節(jié)可知，Extra據(jù)標簽對從OCL規(guī)則庫中獲得符合條件的OCL片段，并組合成了OCL對象屬性集預處理后，OCL 并行查詢剩下的工作就是對對象屬性進行篩選并獲取結(jié)果，需要查詢情況建立對應(yīng)的 MapReduce 任務(wù)。在 MapReduce 任務(wù)中，Mapper 或 Reduc理的對象屬性，是以流的形式傳遞進來的。在 Map 函數(shù)之后，還會有一個洗牌(shu之后才會進行相應(yīng)的 Reduce 任務(wù)進行最終結(jié)果的構(gòu)建。個 OCL 并行查詢包括對象屬性篩選和構(gòu)造查詢結(jié)果兩部分。OCL 查詢會被處理干個 MapReduce 任務(wù)，每個 MapReduce 任務(wù)可以處理一個或多個查詢條件，以象屬性。最后，將篩選出來符合查詢條件的對象屬性進行結(jié)果構(gòu)造，得到最終的結(jié)

【參考文獻】：
期刊論文
[1]分布式XML Twig查詢處理方法[J]. 何志學,廖湖聲,王靜.  計算機工程與設(shè)計. 2016(01)
[2]一種基于GPU的快速XPath查詢算法[J]. 黃玉龍,蘇本躍,奚建清.  計算機應(yīng)用與軟件. 2016(01)
[3]基于MapReduce的XML結(jié)構(gòu)連接處理[J]. 李東,鄧澤航,李祖立.  計算機科學與探索. 2016(08)
[4]基于多謂詞選擇的海量XML數(shù)據(jù)并行查詢方法[J]. 閆威,馬宗民.  小型微型計算機系統(tǒng). 2015(07)
[5]Hadoop迭代優(yōu)化技術(shù)的研究[J]. 王曉軍,鄒亮亮.  計算機技術(shù)與發(fā)展. 2014(09)
[6]MapReduce并行計算技術(shù)發(fā)展綜述[J]. 應(yīng)毅,劉亞軍.  計算機系統(tǒng)應(yīng)用. 2014(04)
[7]一種改進的大規(guī)模CTL公式檢測算法[J]. 奚琪,王清賢,曾勇軍,秦艷鋒.  計算機科學. 2013(10)
[8]MapReduce并行編程模型研究綜述[J]. 李建江,崔健,王聃,嚴林,黃義雙.  電子學報. 2011(11)
[9]云計算:體系架構(gòu)與關(guān)鍵技術(shù)[J]. 羅軍舟,金嘉暉,宋愛波,東方.  通信學報. 2011(07)
[10]云計算和虛擬化技術(shù)[J]. 張耀祥.  計算機安全. 2011(05)

博士論文
[1]實時服務(wù)構(gòu)件的語義特征和行為組裝形式化技術(shù)研究[D]. 金仙力.北京郵電大學 2008

碩士論文
[1]基于云計算平臺的時態(tài)邏輯模型檢測算法研究與實現(xiàn)[D]. 段廷銀.鄭州大學 2016
[2]基于OCL和AOP的面向?qū)ο筌浖到y(tǒng)行為監(jiān)控與驗證研究[D]. 王曉曦.北京工業(yè)大學 2014
[3]形式化B方法驗證技術(shù)研究及其應(yīng)用[D]. 滕騰.揚州大學 2008
[4]基于XML描述的軟件設(shè)計模式實例化研究[D]. 陳賢謀.湖南大學 2005



本文編號：3224059