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

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

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

【學(xué)位級別】：碩士

【部分圖文】：

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

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

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

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

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



本文編號：3224059