Efficient Verification using Generalized Partial Order Analysis

StevenVercauteren,DiederikVerkest,GjaltdeJongandBillLin

IMECLaboratory,Kapeldreef75,B-3001Leuven,BelgiumAlcatelTelecom,F.Wellesplein1,B-2018Antwerpen,BelgiumECEDepartment,UniversityofCalifornia,SanDiego,LaJolla,CA

Abstract

ThispaperpresentsanewformalmethodfortheefficientverificationofconcurrentsystemsthataremodeledusingasafePetrinetrepresentation.Ourmethodgeneralizesuponpartial-ordermethodstoexploreconcurrentlyenabledcon-flictingpathssimultaneously.Weshowthatourmethodcanachieveanexponentialreductioninalgorithmiccomplexitywithoutresortingtoanimplicitenumerationapproach.

1Introduction

Mostmodernembeddedsystemsarenotoriouslydiffi-culttodesign.Despiteutmostcareexercisedbydesigners,initialdesignspecificationsoftencontainsubtle,difficulttodetect,errorsthatresultfromunanticipatedinteractionsbe-tweentheconcurrentparts.Traditionalanalysismethodssuchassimulationareofteninadequateforuncoveringsucherrors,especiallythosethatonlyoccurunderrarecondi-tions.Thus,automatedformalverificationtoolsarebecom-inganindispensablepartofadesigner’stool-box.

In[16]weexplainedhowbothspecificationandimple-mentationofanembeddedsystemcanbeformallyrepre-sentedbythePetrinetformalism[12].Inthispaper,wewillfocusonanovelformalmethodforefficientlyverify-ingconcurrentsystemsmodeledasaPetrinet.Conven-tionalanalysisforPetrinetsmainlyinvolvesareachabilityanalysisoftheunderlyingstatespace.However,therearetwoprimarysourcesofcombinatorialexplosionthatmakesthisconventionalapproachintractableformanyproblemin-stances.

Thefirstsourceisduetoconcurrentlyenabledactions.DuetotheunderlyingunboundeddelayassumptionofPetrinets,concurrentlyenabledactionsmayfireinanyorder.Thisinterleavingsemanticsrequirestheanalysistoenumer-ateallpossibleorderings,whichhasafactorialcomplexitywithrespecttothenumberofconcurrentlyenabledactions.Tocircumventthisproblem,partial-orderanalysis(alsore-ferredtoasstubborn-setoranticipationanalysis)techniqueshavebeendevelopedwhereithasbeenshownthatonlyoneinterleavedsequenceneedstobeanalyzedfordeadlockandlivenesschecks[6,9,14].

Thesecondsourceisduetoconcurrentlymarkedcon-flictplaces.AconflictplacespecifiesachoiceinaPetrinet.Inconventionalanalysis,eachbranchofaconflictplacemustbetraversedindependently.Whentherearemultipleconflictplacesmarkedconcurrently,allpossiblecombina-tionsofpathsmustbeenumerated,whichhasanexponen-tialcomplexitywithrespecttothenumberofconcurrentlymarkedconflictplaces.Thissourceofcomplexityisnotavoidedbypartial-orderanalysistechniques,thusleavingmanyprobleminstancesstillintractable.

Inthispaper,wedescribeageneralizedpartial-orderanalysistechniquethatcanenumerateconflictingpathssi-multaneously,thusextendingthepartial-orderanalysisap-proachtotacklealsothesecondsourceofcombinatorialexplosion.Ourtechniqueisbasedonamodifiedrepresen-tationofmarkingstodistinguishthedifferentconflictingpaths.Thefiringruleshavebeenmodifiedincombinationwiththepartial-orderanalysistechniquetoenumeratecon-flictingpathssimultaneously.Thisnewanalysistechniquecandemonstrateexponentialreductionincomplexity,asil-lustratedbytheexamplesshowninSection4.

Anothertechniquefortacklingthecombinatorialexplo-sionproblemissymbolicanalysis.Symbolicanalysisap-proaches[2,3,5,11]thatimplicitlyenumeratethestatespacehavebeenusedtotacklethecomplexityproblem;theyareeffectivewhenthestatespacebeingtraversedcanbeefficientlyencodedusingbinarydecisiondiagrams.Webelievethisapproachiscomplementarytoourmethodthataimstoaddressspecificationswhosestatespacecannotbeefficientlyencoded.

Theremainderofthispaperisorganizedasfollows.Section2reviewsthebasicdefinitionsandpropertiesofPetrinets,aswellasconventional,partial-orderandsym-bolicanalysistechniques.Section3presentsourgeneral-izedpartial-orderanalysisapproach.Section4discussestheimplementationaspectsandtheresults.ConclusionsaredrawninSection5.

2Background

Inthissectionweprovidesomebackgroundmaterialnecessaryfortheexpositionofourwork.InSection2.1we

reviewbasicdefinitionsandpropertiesof(classical)Petrinets[12].InSection2.2wediscussastraightforwardap-proachtoverificationandtheproblemsinvolved.InSec-tion2.3partial-orderanalysistechniquesarediscussed,aswellastheirlimitations.InSection2.4thesymbolictech-niquesareelaborated.

2.1PetriNets

Definition2.1and,(PetriwithNet)APetrinetisatuple

.

,

Intheabovedefinitiondenotesasetofplaces,asetoftransitions,aflowrelationandaninitialmarking.InFigure1(a),asimplePetrinet(PN)isshown.Theplacesaredepictedwiththeopencircles,thetransitionsarede-pictedwiththeannotatedbars,andtheflowrelationisrep-resentedbythearcs.Theblackdotsrepresenttokens,andtheinitialtokenconfigurationrepresentstheinitialmark-ing.Inthesequel,thesenotationswillbekept.Foraplace

(transition),

anddenotethepresetandpostsetof,thatarereferredtoasthesetofinputandoutputtransitions(places)of,respectively.

Twotransitionsareconflictingoraresaidtobeinconflictwhentheysharecommoninputplaces.Inamaximalcon-flict(ing)set(MCS)alltransitionsthatareinconflictwithatransitionoftheset,arealsoincludedintheset.

Definition2.2Let

.

BesidesthestructureofaPetrinet,thereisalsoanas-sociateddynamics.Astateormarking,isthemappingoftheplacestothenaturalnumbers,indicatingthenumberoftokensintheplaces.Transitionsbetweenstatesaredictatedbythefollowingfiringrule.Inthesequeldenotesthesetofallstates(markings)ofaPetrinetwith

places.

Definition2.3(EnablingRule)Let

and

.

Definition2.4(FiringRule)Let

,

and

true.

ifif

otherwise

Definition2.3statesthatatransitioncanfireifallitsinputplacescontainatleastonetoken.Definition2.4statesthatfiringofremovesonetokeninallitsinputplacesandaddsanewtokeninallitsoutputplaces.

Thesetofallreachablestatesisrepresentedinareacha-bilitygraph,asshowninFigure1(b).InsuchareachabilitygraphallverticescorrespondtoavalidmarkingofthePetri

netandallarcscorrespondtoatransitionfromonemarking

toanotherduetofiringofsometransitioninthenet.ThereachabilitygraphofaPetrinet,denotedas,canthenbeinterpretedasthereflexivetransitiveclosureofthenext-staterelationdefinedinDefinition2.4.

TwoimportantpropertiesofPetrinetsarelivenessandsafeness.Livenessconcernsthequestionwhetheratransi-tioncaneverbefired,andisopposedtodeadlock.Safenessmeansthataplaceshouldnotcontainmorethanonetokenatanytime.InthispaperonlysafePetrinetsareconsidered.

2.2ConventionalAnalysis

Astraightforwardapproachtoverificationistoexplic-itlyenumerateallreachablestates.Reachabilityanalysis,alsoknownasexhaustivesimulationorstatespacegener-ationisindeedapowerfulformalmethodfordetectinger-rorsinconcurrentanddistributedsystemsthathaveafinitestatespace.Adeadlockisthensaidtooccurwhenthereisareachablestatefromwhichthesystem(Petrinet)can-notperformanyaction(transition).Thisapproachhoweversuffersfromthestateexplosionproblem,thatisanexponen-tialincreaseinthenumberofreachablestates.Thesourceofthisexponentialcomplexityareconcurrentlyenabledac-tions(transitions).InPetrinettermsthisisillustratedinFigure1bymeansofanexample.

Petri netState Graphp1p2p3acbabcbcacabp4p5p6cbaFigure1:(a)MarkedPetrinet(b)ReachabilitygraphIntheexampleofFigure1(a),asimplePetrinetisde-pictedresidinginaninitialstateormarkingwheretran-sitions,

andareenabled.Inthisstate,allthreetransitionscanbefiredseparately,eachfiringresultinginanewstate.Ineachofthesenewstates,thetwoothertran-sitionsremainenabledandcanbefired,inturnleadingtotwonewstates.Inthisexample,wethenendupwithdifferentfiringsequencesorinterleavings,ascanbeseeninFigure1(b).Thisfactorialblowupcausesthestatespaceexplosionproblem:especiallyforlargesystemsthatexhibitlotsofconcurrency,thestatespacecanbetoolargewithre-specttothetimeandotherresourcesneededtoinspectallstatesinthespace.

2.3PartialOrderAnalysis

ToverifythelivenesspropertiesofaPetrinet,itcanbeshown[6]thatitisnotnecessarytobuildthecompletereachabilitygraphforanet.Insteadofconstructingallin-terleavingexecutionsequences,onlyafewareneededtoextracttheexternalbehaviorandthesestillcoverthein-ternalnon-determinism.ContinuingwiththeexampleofFigure1(a),supposeweareinthe(depicted)initialstatewheretransitions,,areallenabled.Insteadoffiringalltransitions,inthisstateitisonlynecessarytopursuewithonetransition,atleastiflivenessisthemainconcernofourtofireandanalysis.onlyenabled.Indeed,,forexample.Inturn,thefiringinFinally,theofnextwillkeeptransitionswestateonlyithaveissufficientselectedonequitefactorialpathfromsubstantial.

interleavingthefullreachabilitytolineargraph.interleavings,SowewentwhichfromisThemethodcanalsobeliftedtotransitionsthatareinconflict,thatistransitionsthatsharecommoninputplaces.Supposeinacertainstate,isamaximal(i.e.itcannotbeextended)setofconflictingtransitionsthatareallenabled.Thenitisclear,thatfromthisparticularstate,itissufficienttofireonlythosetransitionsbelongingto,”anticipating”allotherenabledtransitions.Indeed,thelattertransitionsremainenabledafterfiringthetransitionsof,thereforenotaffectingthelivenesspropertiesofthenet.

Themethodhasbeenpresentedindifferentvariants[6,9,14];theyareallbasedontheobservationsdescribedabove.Byusingpartial-ordersemanticsforstate-transitionbasedsystems,theyabstractfromtheinterleavingsemantics.Al-thoughoriginallypresentedtopreservelivenessproperties,themethodcanalsobeusedtodeducesafenesspropertiesofthenetandisevenpartiallyapplicabletomodelcheckingasdescribedin[6,9].

A0B0A0BA0A1B1ANBN1B1A1B1A2B2A2B2A2B2A2B2(a)(b)Figure2:(a)Petrinet(b)“Anticipated”reachabilitygraph

Problem.Thesemethods,however,stillhaveproblemswithconcurrentlyenabledconflictplaces.SupposeamarkedPetrinetasshowninFigure2.InthisexamplePetrinet,wehavepairsofconflictingtransitions(themarkedplacesarecalledconflictplaces).Forthisapplication,thepartial-ordermethodscomputethereachabilitygraphde-pictedinFigure2(b).Itfirstselectsandfires

—i.e.amaximalsetofconflictingtransitionsthatisen-abled—thenputedreachabilitygraph,isandsignificantlysoforth.smallerAlthoughthanthethecom-full

reachabilitygraphitstillresultsinanumberofstatesequaltoFromallthis,.

itisclearthatitwouldbedesirabletonotrestricttheanalysistofiringeachtransitionsequentially,aswithclassicalfiringrulesofPetrinets.Insteadwewouldliketoorderthetransitions,andevaluatepointsatwhichseriesoftransitionscanbefired,sincewedonotneedtoconsiderintermediatesteps,butonlyfinalreachabilityin-formation.

2.4SymbolicReachabilityAnalysis

AnotherapproachtoreachabilityanalysisistouseOr-deredBinaryDecisionDiagrams(OBDD’s)[2]torepre-sentthestategraphsymbolically.OBDD’sareknowntobecompactrepresentationsforsymmetricfunctions.Forapplicationswithnon-linearcommunicationpatterns,how-ever,symbolictechniquesgenerallyperformworse[4],asthenon-linearstructuremakesitdifficulttofindagoodvari-ableorderingfortheOBDD’s.Thus,thestateexplosionproblemcanstillbepresent,especiallyastheencodingofthetransitionfunctionisbasedontheinterleavingseman-tics.

Recently,anapproachwasdescribed[1]thatincorpo-ratedpartial-orderreductionintoanOBDD-basedsymbolicreachabilityanalysis.Whilethismethodimprovesoverstandardsymbolicreachabilityanalysis,itstillrequiresanefficientencodingofthestatespace,whichmaynotex-ist.Wethereforebelievethat[1]iscomplementarytoourmethodthataimstoaddressspecificationswhosestatespacecannotbeefficientlyencoded.

3GeneralizedPartialOrderAnalysis

Inthissectionthekeyideasofourgeneralizedpartial-orderanalysisapproachareelaboratedindetail.Section3.1presentsanintuitiveoverview.Section3.2formallydefinesGeneralizedPetrinets,theworkingvehicleofouranaly-sisapproach.Section3.3discussestheanalysisprocedureitself.

3.1Rationale

Asmentionedinthediscussiononthepartial-ordermethods,forthePetrinetshowninFigure2,thefiringrulesofclassicalPetrinetsrestricttheanalysistofiringeachtran-sitionsequentially.Inthiswork,weovercomethisproblem,byenumeratingconflictingpathssimultaneously.Simplyputtingatokenintheoutputplacesofthefiredtransitionswillnotsuffice,asthiswouldleadtoexecutionsequencesthatarenotpossibleinthe“original”reachabilitygraph,possiblyhidingthepresenceofdeadlocksituations.Itisclearthattherepresentationofthemarkingshastobemod-ifiedtodistinguishthedifferentconflictingpaths.Inthispa-perwethereforepresentamodifiedPetrinetmodel,calledaGeneralizedPetriNet(GPN),thatisclarifiedinFigure3.

p1Ap2CDp5p3p4BConflicting Color Relationintermsofplacesthataremarkedwithcoloredtokens.Inaformalsetting,thesecolorswillberepresentedbytransi-tionsets,todistinguishthedifferentconflictingpaths.Wealsoindicatedthatcolorsmaybeconflicting.Forexample,inFigure3(d)wesuggestedaconflictingcolorrelation,thatstatesthatthecolors“red”and“green”areindeedconflict-ing.Inthefollowing,thiscolorrelationwillberepresented–inthereversesense–byasetofvalidtransitionsets.Definition3.1(GeneralizedPetriNet)AGeneralizedPe-triNetisatuplewith,

,theinitialmarkingand

thevalidtransitionsets.

BesidesthestructureoftheGPNthereisalsoanassoci-ateddynamics.Astateisatuplewheredenotesthemarkingorthemappingoftheplacestothesetsoftran-,anddenotesthesetofallvalidtran-sitionsets

sitionsets.Inthesequelrepresentsasetofplaces,asetoftransitions,andthesetofallstatesofaGPNwith

placesandtransitions.

{}p0A{{A},{B}}p1p2{{A}}p3 B{{B}}Figure4:MarkingofGPNafterfiringAandBsimultane-ously

Toclarifytheabove,imagineaexampleGPNmarkingasillustratedinFigure4.Inthisexample,aGPNmarkingorstateisshownafterfiringandsimultaneously.Theplacesandgetfilledwithand,respec-tively,whileplacebecomesempty—orbettercontainsanemptyset.Theneedforasetofsetsnotationisclearwhenlookingatplace.Thisplacehastwoincomingpaths,andasaresultgets“filled”withtwosetsand

.Associatedwiththisdepictedstate,thereisalsoasetofvalidsets.Forthisexample,

willnotbeavalidset–andthereforenotincludedin–becauseandareconflictingtransitions.Intuitively,avalidsetoftransitionsdenotesasetoftransitionsthatcan“act”togethertoenableandfireacertaintransition.Imag-ineatransitionthathasandasitsinputplaces.Theconflictingtransitionsandcannotacttogethertofiretransition,andthereforeisnotincludedinthesetofvalidsets.Thisinformationcanthenbeusedto“guard”theenablingoftransition,effectivelypreventingthelattertransitionfrombeingfired.TheclassicalPNenablingcon-ditionandfiringruleshavetobechangedassuch,aswillbecomeclearbelow.

LetusreturntoFigure3.Theactionsoffiringandsimultaneously,andoffiring,aretreateddifferently.In

GeneralizedPetrinetsshouldnotbeconfusedwithColoredPetriNets[15].Thelatterareusedinadifferentcontext.Thenotionofcol-orsisintroducedjusttoconveytheidea.

theformercase,thetokensthatarriveintheoutputplacesofandarecolored,astodistinguishtheirmutualexclu-siveorigin.Inthelattercase,noextracoloringisperformed,aswedon’tneedtodistinguishfromaconflictingtransi-tionthatmaybefiredatthesametime(transitioncannotfire!).Thus,forthefiringof,wecanapplyastraightfor-wardextensionofthe“original”PNfiringrule:aredtokenisremovedfromeachofitsinputplacesand,andputintoitsoutputplace.Fromallthis,itisclear,thatinourframeworkweneedtwofiringsemantics,namelyamultiplefiringsemanticsandasinglefiringsemantics.Thesewillbeexplainedhereafter.

SingleFiringSemantics.Accordingtothesinglefiringsemanticsatransitioncanfireonceitissingleenabled.Re-memberfromtheabovediscussion,thatthemarkingofaplaceinaGPNcanbeinterpretedastorepresentallpos-siblehistoriesoftransitionfiringsthatleadtotheinvolvedmarking.Wethensayatransitionissingleenabledwhenitsinputplacescontaina“common”history,oralternatively,whentheintersectionofthetransitionsets,containedinitsinputplaces,isnotempty.Ifso,thefiringofthattransitionwillremovethatcommonhistoryfromitsinputplaces,andputitinitsoutputplaces.

Definition3.2(SingleEnablingRule),

.

Let

SupposeaGPNinastatedepictedinFigure5(a).de-notesthesetofvalidtransitionsets;itsderivationwillbe

describedlaterinmoredetail.Fornow,itsufficestoknowthatisnotavalidsetbecauseandarecon-flictingtransitions.Transitionissingle-enabledas=.Transitionisnot,single-enabledonas

=thecontrary,

.Thus,transitioncanfiretogotothenextstate,accordingtothesinglefiringrule.

{{A},{B}}p0{{A}}p1{{B}}p2{{B}}p0{}p1{{B}}p2Firing of AABAB{}p3{}r = {{A},{B}}p4{{A}}p3{}p4(a)(b)Figure5:Illustrationofthesinglefiringsemantics.(a)Ex-ampleGPNmarkingwithvalidsets(b)

Nextmarkingafterfiringtransition.

Definition3.3(SingleFiringRule)Let=

,

where

.ifif

otherwise

ContinuingwiththeexampleofFigure5(a),iffireswearriveinastatedepictedinFigure5(b).Followingdefini-tion3.3thesetisremovedfromitsinputplacesandandaddedtoitsclassical.NotePNthatfiringthisfiringrule,definedruleisstillinDefinition“consistent”output2.4.withplaceImag-theine,forexample,twoclassicalPNmarkingsbyplacinginFigure5(a)atokenineachplacecontainingor,respectively.ThisresultsinthetwoclassicalPNmarkingsshowninFigure6(a).AnanalogousmappingoftheGPNmarkingdepictedinFigure5(b),resultsinthetwoclassicalPNmarkingsshowninFigure6(b).Notethatthesemark-ingsareexactlythosemarkingsthatcouldbereachedfromthemarkingsshowninFigure6(a)byfiringtransitionus-ingtheclassicalPNfiringrule.Wecanformallydefinetheabovemappingasfollows.

Definition3.4Let

.

NotethatthemarkingofasafePNcanberepresentedbyasetofplaces,whereindicatesthatthereisatokenin.Asaresult,themappingfunctioncanbeinterpretedastomapbetweenastateofaGPNandasetofstatesofasafePNwiththesamestructure.ForFig-ure5,thisgivesand.

ABABFiring of AABABFigure6:ClassicalPNmarkings“equivalent”to(a)Fig-ure5(a)(b)Figure5(b)

MultipleFiringSemanticsAccordingtothemultiplefir-ingsemanticsasetoftransitions-thatmaybeconflicting-canbefiredsimultaneously,providedthateachtransitionismultipleenabled.

Definition3.5(MultipleEnablingRule)Let=,and.

SupposeaGPNinastatedepictedinFigure7(a).Thederivationofthesetofvalidtransitionsetswillbede-scribedlaterinmoredetail.Fornow,itsufficestoknowthatandcannotbeincludedin,be-causeand,aswellasandareconflictingtransi-tions.Weifsayatransitionismultiple.Transitionsenabledinastate

and

asarethenmultipleenabled=inthedepicted,state,thatwhenatransitionismultiple=enabled,itisalso.singleNote

and

enabled(thereverse,however,isnotalwaystrue).Thus,canbefiredsimultaneously,bothandaccordingaremultipletothemultipleenabled,firingandinthestaterule.

r0{}{}p0p0p0ABABAB{}r0{}{{A,C},r{{B,C},{}p1p2 {A,D}}p10(=r1)p2 {B,D}}{}p1p2{}p3p3CDCDp3CD{}p5{}p5{}p5{{A,C},{B,D}} = {r(a)0{A,C},{B,C},{A,D},{B,D}}r(b)1={A,C},{B,C},{A,D},{B,D}}r(c)2={{A,C},{B,D}}state statestate Figure7:SubsequentmarkingsofaGPNwithmaxi-malconflicting(c)

(b)

setsand.(a)initialstate

Definition3.6(MultipleFiringRule)Let=

,andsuchthat

=true.

where

otherwise

ContinuingwiththeexampleofFigure7(a),thesimultaneousfiring(=oftransitionsandmoves)and

commoninputplace,to(=theiroutputplaces)andfromtheir

,re-spectively.Assuch,wearriveinthestateinFigure7(b).Theupdatingofthesetofvalidsetsdepictedhasnoeffectinthiscase,as.Aswiththesinglefiringse-mantics,onecanalsoobservetheconsistencywithclassicalPNdynamics.Indeed,asmarkingcanbemappedtothemarkingofaclassical(safe)PNwhereplacesandcontainatoken.Themarking,however,canbemappedto2classical.Note

PNmarkingsthatthelattermarkingscanbereachedfrombyseparatelyfiringandusingtheclassicalPNfiringrule.Thesameobservationcanbemadewhengoingtothenextstate;transitionstothenext-stateandcanandbearebothmultipleenabledinstatetotheextraconditioningof,depictedfiredsimultaneouslybyinFiguretogo,the7(c).newDuesetofvalidsetsnowbecomesaresult,

statecal(safe)PNwherecanbeonlymappedplacestothe,andthe.newAs

containsmarkingaoftoken;aclassi-i.e.themarkingthatcanbereachedfrom

PNfiringrule.Theextrabyfiringconditioningandusingofthethesetclassical

ofvalidsetsrulesoutand,infactmodelingan”ex-tendedandandconflict”conflicts,respectively.relationbetweenIndeed,ifand(),andbetween(with)cannot,thenbeincluded()conflictsprecedes()inanyvalidwithset.

()and

3.3AnalysisProcedure

SupposenowasafeclassicalPN

andaGeneralizedPetriwith

netwiththesamestructure

if

otherwise

thenitisclearthatconflictingtransitionscanbepartofanyvalidset.andOnenotwo

canthenproceedwithingSets(MCS’s).wethesearchreachabilityAcandidateforcandidateanalysisasfollows.InstateMCSMaximalmustbeConflict-multipleenabled,andfiringwillnotdisableanyotherMCSthatwasalreadymultipleenabled,aswellasanyothertransition

thatwassingleenabled.Asaresult,thesamereduc-tiontechniquesofthepartial-ordermethodscanbeapplied:selectingonlyoneinterleavingsequence,oralternatively,firingallcandidateMCS’satthesametimeandpostponingthepossiblefiringoftheothertransitionstoafuturestate.Moreover,oneisguaranteedthatthereachedstatecanbemapped.toasetofstatesofthe”original”reachabilitygraph

IfinstateonehastofallbackonthenosinglecandidatefiringMCS’ssemanticscanbeandfound,againapplypartial-orderreductions,ifpossible.Similarly,withthesinglefiringrule,oneisguaranteedtobe”intrack”withclassicalPNdynamics.

Thesamereasoningappliestoallnextreachablestates.Byinduction,onecanthenconcludethatthefollowingalgorithmcomputesenoughofthereachablestatesofa

Astonotclutterthealgorithm,weleftoutthecodethatchecksa.o.thatthefiringofanenabledtransitionisnotpostponed“forever”.

GPNtodecideaboutthebehaviorofasafePNwiththesamestructure.

Apropertythatisoftencheckedforisthefreedomofdeadlock.Inthisframework,thedefinitionofadeadlockischaracterizedby:

single-execute(G,s,t)

in:anetN=P,T,F,,astates=m,r,atransitiontthatissingleenabledinstatesbegin

lets’=supdate(s,t)add(s,t,s’)toRGifs’RG

thenreach(N,s’)Effectively,thisboilsdowntocheckingupon

AlgorithmGeneralizedPartial-OrderReachabilityAnalysisglobal:RG

reachabilitygraph

reachability-graph(N,m)

in:atupleN=P,T,F,amarkingmsuchthatP,T,F,mPetrinetbegin

letm

if

otherwise

letr=

lets=m,rRG=[s,,reach(N,s)s]end

reach(N,s)

in:atupleN=P,T,F,astates=m,rbegin

letsingle-enabled-trans=tTsenabled(t,s)Searchforcandidate-mcs

if

senabled(t,s)

r

thenreportdeadlockpossibilityatstateselseifcandidate-mcs

thenmultiple-execute(N,s,candidate-mcs)

elseifT’single-enabled-trans:T’mcs(T))

thenforalltT’do

single-execute(N,s,t)od

elseforalltsingle-enabled-transdo

single-execute(N,s,t)od

fififiend

multiple-execute(N,s,mcs)

in:atupleN=P,T,F,astates=m,r,asetmcsofmaximalconflictingsetsthataremultipleenabledinstatesbegin

letT’=

lets’=mupdate(s,T’)add(s,T,s’)toRGifs’RG

thenreach(N,s’)fiend

fiend

4ImplementationandResults

Thetechniquespresentedinthispaperhavebeenim-plementedinatool,calledJULIE,inaboutlinesofCcode.Toassesstheviabilityofourapproach,wehaveisasafe

carriedoutanumberofexperimentsthatsufferfromthestateexplosionproblem.Theanalyzedexampleswerethenon-serializedversionofthewell-knownDiningPhiloso-phersProblem(NSDP)[6],theAsynchronousArbiterTree(ASAT)[1],theOvertakeProtocol(OVER)[4],andRead-ersandWriters(RW)[4].

Tocomparewithstate-of-the-artverificationtools,wehavechosenSPINextendedwiththePartial-OrderPack-age(SPIN+PO)[8],andtheSymbolicModelVerifier(SMV)(Release2.4.4)[10],asrepresentativesofthepartial-ordermethodsandthesymbolictechniques,respectively.Weusedbothpackages,aswellasourprototypeGeneral-izedPartialOrderAnalysistool,totesttheexamplesfordeadlocksituations.However,obtainedresultsarealsovalidforsafetychecks,sincetheverificationofasafetypropertycanalwaysbereducedtoacheckfordeadlock[9].AnumericoverviewoftheresultsisshowninTable1.InTable1thenumberofstatesofthecompletereacha-bilitygraph,thenumberofstatesofthereachabilitygraphsderivedusing(generalized)partial-orderanalysis,aswellthepeakBDDsizesencounteredduringsymbolicreacha-bilityanalysis,arelistedforvariousinstancesoftheparam-eterizedexamples.CPUtimes,measuredonaHPK260with896MBRAM,arealsoincluded.

ForNSDP,ASATandOVER,generalizedpartial-orderanalysisoutperformsbothSPIN+POandSMV.AdrasticimprovementpendentstatesareofthesufficientisobservedforNSDPandASAT.ForNSDPnumbertoofdetectphilosophers.alldeadlockAscansituations,beobserved,inde-CPUtimesincreaselinearlywithproblemsize.

ForRW,generalizedpartial-orderanalysisperformsbet-terthanSPIN+PO,butslightlyworsethanSMV.Thisisbe-causeRWexhibitsalotofconditionalbehaviorwherenonoftheclassicalpartial-orderreductiontechniquescanbeap-plied–thisisalsovisibleinthereducedstatespacewhichequalsthecompletestatespace.Forthisproblem,OBDD’sapparentlyprovideanefficientencodingofthestatespace.

Table1:ResultsofGeneralizedPartialOrderAnalysis(GPO)

Problem(size)NSDP(2)NSDP(4)NSDP(6)NSDP(8)NSDP(10)ASAT(2)ASAT(4)ASAT(8)OVER(2)OVER(3)OVER(4)OVER(5)RW(6)RW(9)RW(12)RW(15)

States

SPIN+POStatesTime(s)

SMV

PeakBDD-sizeTime(s)

GPO

StatesTime(s)

hours

hours

5Conclusions

Inthispaperwepresentedanovelgeneralizedpartial-orderanalysistechniquethatcanenumerateconflictingpathssimultaneously,thusextendingthepartial-ordertech-niques[6,9,14]totacklealsotheexplosionproblemduetoconcurrentlymarkedconflictplaces.TheapproachisbasedonaGeneralizedPetriNetmodelthathasamodifiedmarkingrepresentationtodistinguishthedifferentconflict-ingpaths.

Theexperimentalresultsareverypromising.Asillus-tratedinSection4,forcertainexamplesonecandemon-strateexponentialreductionincomplexity.Themethodhasbeenappliedtosomereal-lifeapplicationsinembeddedsystemdesign(e.g.aQuadratureAmplitudeModulationmodem),whereitalsoprovidedsignificantgain[16].

Recently,anumberofinterestingmethods[7,13]havebeenproposedfortheefficienttimingverificationofcon-currentsystems,modeledasTimedPetrinets.Wearecur-rentlyinvestigatinghowthesemethodscanbeleveragedtoourwork.

[4]J.C.Corbett.EvaluatingDeadlockDetectionMethodsforConcurrentSoftware.

IEEETransactionsonSoftwareEngineering,22(3):161–180,March1996.[5]O.Coudert,J.C.Madre,andC.Berthet.VerifyingTemporalPropertiesof

SequentialMachinesWithoutBuildingtheirStateDiagrams.InWorkshoponComputer-AidedVerification,Rutgers,June1990.[6]G.G.deJong.GeneralizedDataFlowGraphsTheoryandApplications.Ph.D.

Thesis,TechnicalUniversityofEindhoven,October1993.[7]G.deJongE.VerlindandB.Lin.EfficientPartialEnumerationforTimingAnal-ysisofAsynchronousSystems.InProceedingsofthe33rdDesignAutomationConference,pages55–58,June1996.[8]P.GodefroidandD.Pirottin.RefiningDependenciesImprovesPartial-Order

VerificationMethods.InC.Courcoubetis,editor,Proceedingsofthe5thInter-nationalConferenceonComputerAidedVerification,pages438–449,Elounda,Greece,1993.[9]P.GodefroidandP.Wolper.UsingPartialOrdersfortheEfficientVerificationof

DeadlockFreedomandSafetyProperties.LectureNotesinComputerScience,575(10):332–342,Aalborg,Denmark,July1-41991.[10]K.L.McMillan.SymbolicModelChecking.KluwerAcademicPublishers,

Boston,1993.[11]E.Pastor,O.Roig,J.Cortadella,andR.M.Badia.PetriNetAnalysisusing

BooleanManipulation.LectureNotesinComputerScience815,SpringerVer-slag,pages416–435,June1994.[12]J.L.Peterson.PetriNetTheoryandModellingofSystems.PrenticeHall,1981.[13]A.SemenovandA.Yakovlev.VerificationofAsynchronousCircuitsusing

TimePetriNetUnfolding.InProceedingsofthe33rdDesignAutomationCon-ference,pages55–58,June1996.[14]A.Valmari.AStubbornAttackonStateExplosion.In2Workshopon

ComputerAidedVerification,pages156–165,NewBrunswick,NJ,June18-211990.

References

[1]R.Alur,R.K.Brayton,T.A.Henzinger,andS.QadeeramdS.K.Rajamani.

Partial-orderReductioninSymbolicStateSpaceExploration.InProceedingsoftheInternationalConferenceonComputerAidedVerification,1997.[2]R.R.Bryant.Graph-basedAlgorithmsforBooleanFunctionManipulation.

IEEETransactionsonComputers,35(8):677–691,August1986.[3]J.R.Burch,E.M.Clarke,K.L.McMillan,andD.L.Dill.SequentialCir-cuitVerificationUsingSymbolicModelChecking.InProceedingofthe27thACM/IEEEDesignAutomationConference,Orlando,June1990.

[15]J.Vautherin.ParallelSystemsSpecificationswithColoredPetriNetsandAlge-braicSpecifications.AdvancesinPetriNets1987,LectureNotesinComputerScience266,pages293–308,1987.[16]S.Vercauteren,D.Verkest,G.deJong,andBillLin.DerivationofFormal

RepresentationsfromProcess-basedSpecificationandImplementationModels.InTheProceedingsoftheInternationalSymposiumonSystemSynthesis,pages16–23,September1997.