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

【摘要】：面向服務(wù)的體系結(jié)構(gòu)(SOA),它是一種新的可以支持分布式計(jì)算的范型,而Web服務(wù)就是這種面向服務(wù)的體系結(jié)構(gòu)的具體表現(xiàn)形式之一。根據(jù)Web服務(wù)的動(dòng)態(tài)性特征以及分布式的特點(diǎn),使用Web服務(wù)組合可以非常有效的組裝網(wǎng)絡(luò)中存在的多種分布式跨平臺(tái)下的異構(gòu)服務(wù),以實(shí)現(xiàn)多種異構(gòu)服務(wù)間的信息共享,最終形成具備強(qiáng)大功能的Web服務(wù)流程用以適應(yīng)現(xiàn)在復(fù)雜的企業(yè)網(wǎng)路環(huán)境。然而在復(fù)雜的網(wǎng)絡(luò)環(huán)境下,如何在Web服務(wù)系統(tǒng)投入運(yùn)行之前就發(fā)現(xiàn)Web服務(wù)系統(tǒng)中存在的嚴(yán)重問題,如何確保在分布式的Web服務(wù)系統(tǒng)中獲取一個(gè)可信的服務(wù),確保服務(wù)上線后的正確性,對(duì)服務(wù)的測(cè)試是至關(guān)重要的。如果按照傳統(tǒng)的測(cè)試方法,就必須對(duì)每個(gè)子服務(wù)做窮舉性測(cè)試,分別為每個(gè)子服務(wù)準(zhǔn)備相應(yīng)的測(cè)試套。如果系統(tǒng)中的子系統(tǒng)數(shù)量很多,測(cè)試工作會(huì)變的非常耗時(shí)。用LOTOS建模語言對(duì)這種具有分布式特點(diǎn)的Web服務(wù)系統(tǒng)建模是一種非常有效的方式,首先采用形式化方法來描述Web服務(wù)組合的系統(tǒng),然后從模型上面對(duì)系統(tǒng)進(jìn)行模型檢測(cè),通過系統(tǒng)屬性對(duì)模型進(jìn)行驗(yàn)證來縮小問題域,找到具體的可能存在缺陷的服務(wù)做測(cè)試,實(shí)現(xiàn)模型檢測(cè)與測(cè)試的結(jié)合,可以高效的保證服務(wù)的可靠性。 模型檢測(cè)與測(cè)試混合方法是保證服務(wù)可靠性的一種效果顯著的方法,采用形式化建模語言LOTOS對(duì)Web服務(wù)組合后的BPEL流程進(jìn)行建模,然后使用CADP工具集中提供的模型檢測(cè)器Evaluator對(duì)建立好的LOTOS模型進(jìn)行驗(yàn)證,通過屬性檢驗(yàn)縮小問題域,最后用TTCN3測(cè)試語言描述滿足模型檢測(cè)反例的測(cè)試用例,完成最后的測(cè)試工作,并最終對(duì)整個(gè)模型檢測(cè)與測(cè)試相結(jié)合的測(cè)試流程所涉及到的測(cè)試工具進(jìn)行集成,以支撐整個(gè)測(cè)試流程。Web服務(wù)組合的LOTOS建模和基于模型檢測(cè)反例以及相應(yīng)服務(wù)的WSDL描述的TTCN3抽象測(cè)試套的生成是實(shí)現(xiàn)模型檢測(cè)與測(cè)試混合方法的兩個(gè)難點(diǎn)。 本文提出模型檢測(cè)與測(cè)試混合方法,并給出模型檢測(cè)與測(cè)試相結(jié)合的測(cè)試流程。實(shí)現(xiàn)這種測(cè)試流程,首先要進(jìn)行WEB服務(wù)組合的LOTOS建模。為了保證基于模型檢測(cè)反例的測(cè)試有意義,必須解決對(duì)LOTOS模型進(jìn)行模型檢測(cè)生成的反例缺乏測(cè)試數(shù)據(jù)的問題,由此本文給出了LOTOS復(fù)雜數(shù)據(jù)類型擴(kuò)展方法和WSDL服務(wù)的LOTOS建模過程中測(cè)試數(shù)據(jù)的生成方法,使得基于反例生成的TTCN3抽象測(cè)試套能夠擁有測(cè)試數(shù)據(jù)。本文在前期工作的基礎(chǔ)上實(shí)現(xiàn)LOTOS建模和基于模型檢測(cè)反例的TTCN3測(cè)試套的自動(dòng)生成,最終實(shí)現(xiàn)模型檢測(cè)與測(cè)試的結(jié)合,并對(duì)已有的工具進(jìn)行集成。最后結(jié)合Web服務(wù)實(shí)例,驗(yàn)證該集成工具所執(zhí)行的測(cè)試流程的可行性。
[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.
【學(xué)位授予單位】：北方工業(yè)大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2014
【分類號(hào)】：TP393.09;TP311.53

【參考文獻(xiàn)】

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

1 劉衛(wèi)東,宋佳興,林闖;基于價(jià)格時(shí)間Petri網(wǎng)的網(wǎng)格計(jì)算應(yīng)用模型及分析[J];電子學(xué)報(bào);2005年08期

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

3 楊敬峰,蔣凡;協(xié)議測(cè)試標(biāo)準(zhǔn)TTCN-3的實(shí)現(xiàn)[J];計(jì)算機(jī)工程與應(yīng)用;2004年05期

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

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

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

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

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

9 胡春華;吳敏;謝R，

本文編號(hào)：2037901