1、湖北大學(xué)碩士學(xué)位論文高級(jí)Petri網(wǎng)的測(cè)試方法研究姓名：劉艷申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：系統(tǒng)分析與集成指導(dǎo)教師：周雙娥20070501AbstractPetrinetshavebeenextensivdyusedinthemodelingandanalysisofconcurrentanddistributedsystemsTheverificationandvalidationofPetrinetsaleofpanicul盯importa

2、nceinthedevelopmentofconcurrentanddistributedsystemsBesidesformalanalysistechniquestestinghasbeenproventobeeffectiveindetectingsystem鋤侶andiseasytoapplyAnapproachoftestingPetrinetssystematicallyandeffectivelyistodevelopte

3、stcriteriaSOthattestadequacy啪bemfa蛐l(wèi)edobjectivelyInthis弘咿％wemainlytestahighlevelPeUinetPredicate／Transitionnet(Pr／tnet)，Pr／tnetissuitablefordefiningcontrol，datafunctionanddynamicbehaviourofbasicconcmrentsystemFirstlythis

4、paperexplainsthebasicknowledgeaboutPetrinetandtestingOnhighlevelPetrinets，itdiscussesthesyntaxandstaticsemantic，dynamicsemanticsandobservablebehaviourNextitpresentsgtatoorientedtestingandhansitionorientedtastingafterexpl

5、ainingthebasicknowledgeaboutPetrinetandtestingSecondlyitinvestigatesthemedlodofobservingandrecordingtestingresults，andgivesasetofcoveragecriteriatomeasI玳testadequacyThirdlyitgivesanexampleofdiningphilosophers’problemAcco

6、rdingthetechnologiesofmodelingthediningphilosophers’problem’sPrfrmodelhasbeenestablishedFourthlyitteststhemodelusingstateorientedtestingandtransitionorientedtestingmethodThenitintroducesamodelchoikertoolSPIN(SimplePmmela

7、Interpreter)Spinisapopularopensourcesoftwaretoolthat啪beusedfortheformalverificationofdistributedsoftwaresystemsSpinsupportsahighlevellanguagetospecifysystemsdescriptiOtiS，calledPROgELA(aPROcessMEtaLAnguage)Sixthlyinthisp

8、aperdiningphilosophers’problem’sPr／rnetistranslatedintoequivalentSpinmodels—Promelaprograms，andrunstheprograminXspmwhichneedstheenvironmentofvimmlLinuxunderCygwinInsimulation，itcannoticethatindiningphilosophers’problem’s