發(fā)布時間：2018-06-19 02:17

  本文選題：模型檢測 + 測試��； 參考：《北方工業(yè)大學》2014年碩士論文

【摘要】：面向服務(wù)的體系結(jié)構(gòu)(SOA),它是一種新的可以支持分布式計算的范型,而Web服務(wù)就是這種面向服務(wù)的體系結(jié)構(gòu)的具體表現(xiàn)形式之一。根據(jù)Web服務(wù)的動態(tài)性特征以及分布式的特點,使用Web服務(wù)組合可以非常有效的組裝網(wǎng)絡(luò)中存在的多種分布式跨平臺下的異構(gòu)服務(wù),以實現(xiàn)多種異構(gòu)服務(wù)間的信息共享,最終形成具備強大功能的Web服務(wù)流程用以適應現(xiàn)在復雜的企業(yè)網(wǎng)路環(huán)境。然而在復雜的網(wǎng)絡(luò)環(huán)境下,如何在Web服務(wù)系統(tǒng)投入運行之前就發(fā)現(xiàn)Web服務(wù)系統(tǒng)中存在的嚴重問題,如何確保在分布式的Web服務(wù)系統(tǒng)中獲取一個可信的服務(wù),確保服務(wù)上線后的正確性,對服務(wù)的測試是至關(guān)重要的。如果按照傳統(tǒng)的測試方法,就必須對每個子服務(wù)做窮舉性測試,分別為每個子服務(wù)準備相應的測試套。如果系統(tǒng)中的子系統(tǒng)數(shù)量很多,測試工作會變的非常耗時。用LOTOS建模語言對這種具有分布式特點的Web服務(wù)系統(tǒng)建模是一種非常有效的方式,首先采用形式化方法來描述Web服務(wù)組合的系統(tǒng),然后從模型上面對系統(tǒng)進行模型檢測,通過系統(tǒng)屬性對模型進行驗證來縮小問題域,找到具體的可能存在缺陷的服務(wù)做測試,實現(xiàn)模型檢測與測試的結(jié)合,可以高效的保證服務(wù)的可靠性。 模型檢測與測試混合方法是保證服務(wù)可靠性的一種效果顯著的方法,采用形式化建模語言LOTOS對Web服務(wù)組合后的BPEL流程進行建模,然后使用CADP工具集中提供的模型檢測器Evaluator對建立好的LOTOS模型進行驗證,通過屬性檢驗縮小問題域,最后用TTCN3測試語言描述滿足模型檢測反例的測試用例,完成最后的測試工作,并最終對整個模型檢測與測試相結(jié)合的測試流程所涉及到的測試工具進行集成,以支撐整個測試流程。Web服務(wù)組合的LOTOS建模和基于模型檢測反例以及相應服務(wù)的WSDL描述的TTCN3抽象測試套的生成是實現(xiàn)模型檢測與測試混合方法的兩個難點。 本文提出模型檢測與測試混合方法,并給出模型檢測與測試相結(jié)合的測試流程。實現(xiàn)這種測試流程,首先要進行WEB服務(wù)組合的LOTOS建模。為了保證基于模型檢測反例的測試有意義,必須解決對LOTOS模型進行模型檢測生成的反例缺乏測試數(shù)據(jù)的問題,由此本文給出了LOTOS復雜數(shù)據(jù)類型擴展方法和WSDL服務(wù)的LOTOS建模過程中測試數(shù)據(jù)的生成方法,使得基于反例生成的TTCN3抽象測試套能夠擁有測試數(shù)據(jù)。本文在前期工作的基礎(chǔ)上實現(xiàn)LOTOS建模和基于模型檢測反例的TTCN3測試套的自動生成,最終實現(xiàn)模型檢測與測試的結(jié)合,并對已有的工具進行集成。最后結(jié)合Web服務(wù)實例,驗證該集成工具所執(zhí)行的測試流程的可行性。
[Abstract]:Service-Oriented Architecture (SOA) is a new paradigm that supports distributed computing, and Web Services is one of the concrete manifestations of this Service-Oriented Architecture. According to the dynamic and distributed characteristics of Web services, using Web services composition can effectively assemble heterogeneous services under distributed cross-platform in network, so as to realize the information sharing among heterogeneous services. Finally, a powerful Web service process is formed to adapt to the current complex enterprise network environment. However, in the complex network environment, how to find the serious problems in the Web service system before it is put into operation, and how to ensure the acquisition of a trusted service in the distributed Web service system. Ensuring the correctness of the service after it is online is critical to the testing of the service. If we follow the traditional test method, we must make exhaustive test for each sub-service and prepare the corresponding test suite for each sub-service. If the system has a large number of subsystems, testing can become very time-consuming. Lotos modeling language is a very effective way to model this distributed Web service system. Firstly, a formal method is used to describe the Web service composition system, and then the model checking is carried out on the model facing the system. The system attributes are used to verify the model to narrow down the problem domain, to find the specific service that may have defects, and to realize the combination of model checking and testing, which can effectively guarantee the reliability of the service. The mixed method of model checking and testing is an effective method to ensure the reliability of service. Lotos is used to model the BPEL process after Web services composition. Then the model detector Evaluator provided by CADP tool set is used to verify the established Lotos model, and the problem domain is reduced by attribute checking. Finally, TTCN3 test language is used to describe the test cases that satisfy the model checking counter cases, and the final test work is completed. Finally, it integrates the testing tools involved in the testing process of the whole model detection and testing. Lotos modeling which supports the whole testing process. Web services composition and TTCN3 abstract test suite generation based on model checking counterexample and WSDL description of corresponding services are two difficulties in implementing the mixed method of model checking and testing. In this paper, a hybrid method of model checking and testing is proposed, and the test flow of model checking and testing is given. To implement this testing process, the Lotos modeling of Web service composition should be carried out first. In order to ensure that the counterexample test based on model checking is meaningful, it is necessary to solve the problem that the counterexample generated by model checking of Lotos model lacks test data. In this paper, the extension method of Lotos complex data types and the method of generating test data in Lotos modeling of WSDL services are given in this paper, so that the TTCN3 abstract test suite generated by counterexample can have test data. In this paper, Lotos modeling and TTCN3 test suite automatic generation based on model checking counterexample are realized on the basis of previous work. Finally, the combination of model checking and testing is realized, and the existing tools are integrated. Finally, a Web service example is used to verify the feasibility of the test process executed by the integration tool.
【學位授予單位】：北方工業(yè)大學
【學位級別】：碩士
【學位授予年份】：2014
【分類號】：TP393.09;TP311.53

【參考文獻】

相關(guān)期刊論文 前10條

1 劉衛(wèi)東,宋佳興,林闖;基于價格時間Petri網(wǎng)的網(wǎng)格計算應用模型及分析[J];電子學報;2005年08期

2 張君華;黃志球;曹子寧;;模型檢測基于概率時間自動機的反例產(chǎn)生研究[J];計算機研究與發(fā)展;2008年10期

3 楊敬峰,蔣凡;協(xié)議測試標準TTCN-3的實現(xiàn)[J];計算機工程與應用;2004年05期

4 張寧寧;劉孟仁;;模型檢測在軟件測試中的應用[J];計算機與數(shù)字工程;2006年02期

5 李立綱;李銀勝;;基于代理和BPEL4WS的Web服務(wù)合成與實現(xiàn)[J];計算機應用與軟件;2007年06期

6 趙會群;何霞;;基于翻譯模式的BPEL到LOTOS映射方法研究[J];計算機應用研究;2013年06期

7 倪悅;范玉順;;基于著色Petri網(wǎng)的語義Web服務(wù)組合形式化驗證[J];清華大學學報(自然科學版);2010年05期

8 柳毅;麻志毅;何嘯;邵維忠;;一種從UML模型到可靠性分析模型的轉(zhuǎn)換方法[J];軟件學報;2010年02期

9 胡春華;吳敏;謝R，

本文編號：2037901