搜索
ISSN100021239PCN1121777PTPJournalofComputerResearchandDevelopment46(7):114321151,2009:2008-04-27;:2008-06-27:(60773064);(2006AA01Z167,2006AA04Z165,2006AA04Z150)1,2111(150001)2(361021)(lihaibo@hit.edu.cn)IntegrationVerificationofWorkflowBusinessRuleSemanticLiHaibo1,2,ZhanDechen1,andXuXiaofei11(ResearchCenterofIntelligentComputingforEnterprises&Service,SchoolofComputerScienceandTechnology,HarbinInstituteofTechnology,Harbin150001)2(CollegeofComputerScience&Technology,HuaqiaoUniversity,Xiamen,Fujian361021)AbstractWorkflowmodelmustbedescribedcorrectlytoguaranteesuccessfulexecutionatruntime.Soverificationtechnologyofmodelisimportantandcanbeclassifiedintosyntactic,structural,andsemantic.Thestrictestandhighest2levelverificationisthesemanticonewhichhasnotbeensolvedwellyetintheworkflowresearch.Futhermore,correctnessofcontrollogicdependsonbusinesssemantic,andisoneoftheinfluencefactorsonstructualsoundness.Byanalyzingbusinessrulesandtheirconstraintpartsdescribedinworkflowmodel,businessrulessemanticcanbeformalizedtoexpression.Soverifyingsemanticintegralityofbusinessrulescanbeconvertedintothatofconstraintsets.Constraintsetsareusedtodecidewhichpathischosentoexecute.Ifaconstraintsetdescribedinaconditionnodeinworkflowmodelmissessomesemanticsandexpressesredundantormeaninglesssemantics,thesecanalsocauseerroneousstructure,whichisoneoftheimportantfactorsexecutingunsuccessfully.Domainofuniversecoverabilitytheoremanddecision2tree2basedverificationarithmeticareputforwardtoverifythesemanticintegralityofconstraintsets,andthenthestructrualsoundnessofworkflowmodelisensuredbythismethod.Thisverificationtechnologyisindependentofspecificmodelingmothods,sothatcompletecommonality,modeling2independentce,andwideapplicabilityarethethreeadvantagesofthisverificationmethod.Keywordsworkflow;businessrule;semanticintegration;verification;domainofuniversecoverability,,,,.,,.,,,.,.,,.,,.;;;;TP311,,,.,.[1],,,,.,,,.,[2],3.,,(soundness)[327],,,.,:well2structure,coverability,boundness,liveness,reachability,safety,strongconnection,deadlock,[328],.,,Petri.,,[8].,,,,.,,:1).,,,.UML,Petri,,.2).,,[9],,.3).[10212],,,,.,,,,,.1,,.[13].,:.,,.,,,..,(),.,,(XOR),(OR)[14],XOR,.,44112009,46(7).,,,,1(a).,,,,.1(b),5000,5000,,.,,,1(c):,.Fig.1Semanticintegrationofworkflowbusinessrulesset.(a)Missingsemantic;(b)Redundantsemantic;and(c)Meaninglesssemantic.1.(a);(b);(c),,,,.2,.,(WfMC)6,:(sequence)(AND2split)(AND2join)(OR2split)(OR2join)(iteration),,,[14]21,.(XOR,WfMCOR),,,.:M,M(XOR),COND={cond1,cond2,,condn},condiCOND,,COND,.1....1.COND,,.c1()=,c2()=,c1c2,:c1c2c1.,,COND,,.2..CONDcond(CO)COND,CO={co1,co2,,com},cond(CO)CODD,DDCO,Dom(cond(CO))=DD.,COND={c1c2,c1c2,c1},c1c2,D={=and=},D={=or=}.3..COND={cond1,cond2,,condn},condi(CO)COND,CO={co1,co2,,com},condi(CO)CODi,CONDn-15411:cond1(CO),cond2(CO),,condi-1(CO),condi+1(CO),,condn(CO),COD1,D2,,Di-1,Di+1,,Dn,Dom(condi(CO))=D1,,Dn,CONDCO.,..condi,condiDi,Di.3,XOR,,,.1..,COND={cond1,,condn}..,CONDCO,COND.1).condi(x1,x2,,xm-1),1in,xmcondi,xncondi,condi(x1,x2,,xm-1)condi(x1,x2,,xm),CO={x1,x2,,xm}.2).Dom(condi)D1D2Dm,1in,:Dom(condi)D1D2Dm,DD1D2Dm,Dom(condi)=D1D2Dm-D,D,,DDom(condi).D1D2DmDom(condi),D,DD1D2Dm=Dom(condi),CONDDcond...,COND={c1c2,c1c2,c1},c1,c2,c1c2c1c2:D1={=and=};D2={=and=};c1D3={=},D1D2D3COND,COND..4,,,.,COND,,,,:,,,.(,P1()5000,P2()5000and10000,P3()10000,P1,P2P3P),,,P1,P2P3,3,,,.COND,,,,,.,,COND.,COND,.,COND,,COND,COND,COND.64112009,46(7),.1.COND..,.COND={cond1(x1,x2,,xn),cond2(x1,x2,,xn),,condm(x1,x2,,xn)},x1,x2,,xn,,condiP(1im),m-1condjP(1jm-1,condicondj),COND,Dom(cond1)=Dom(cond2)==Dom(condm)..,,..,,c1()c2()c.COND={ci|ci=ci1ci2cim,1in},cij(1jm),.cij(1jm),C=c11c12c1mc21c22c2mcn1cn2cnm,c11,c21,,cn1,CCOND.Ccij,cijwij=1,wij=0,Cp,,W=(w1,w2,,wp).1.DC.:CONDC;:F.1)F0={T1,T2,,Tp},:Cpp,TiCci(1ip),Tic1i,c2i,,cxi(c1i,c2i,,cxiCci),;2)Wwj=min(W)(1jp)F0Tj,F,F0Tj,Wwj;3)W,8);4)Wwk=min(W)(1kp),FTk:TkF0,ckC,TjFck,c1k,c2k,,cyk(c1k,c2k,,cykCck);5)F0Tk,TkF;6)Wwk;7)W,4)5)6);8):Cc,Fcijcj,c=cj,marked;9)Fmarked,cijcj=c,cC,marked,F.:CONDXOR,COND,,AND.CONDC,:1)Cci,cj(ciCOND,cjCOND,1in,1jn,ij),ci=cj,COND.,XORAND,2(a).C2(c),.2)CC1C2,C1C2.C1C2,,,2(b).C3C4,C4,C2AC1,C2(d),.,F7411:,.F,,COND.F,,,COND.Fmarked,COND,.Fig.2Concurrencyimpliedinconstraintset.22..COND,DCF,CONDF,COND,..1)DCFCOND.Cm,p,ciNi.4)5),mp,1pN1N2NpF.FN1N2Np,FCOND.2)CONDFCONDF,COND,8)9).:8)FCOND.cCOND,cF,c|CONDF,CONDACONDF,COND.8)marked9),,CONDACONDF.3)F,COND.CONDACONDF,COND,F.markedckCONDF,ciCOND,cick,CONDck,,.4)CONDF,COND.F,COND,CONDF,COND,..5,,,.,1,COND2.84112009,46(7)Table1ConstrainedObjectsandTheirDomainofUniverseforCustomerOrderChanged1ConstrainedObjectAtomicPredicationDeliverstateDLV1:Deliverstate=DeliveredDLV2:Deliverstate=NotdeliveredProducestatePD1:Producestate=ProducedandnotcompletedPD2:Producestate=NotproducedPD3:Producestate=ProducedandcompletedSupplierdeliverstatePVD1:Supplierstate=SupplierdeliveredPVD2:Supplierstate=SuppliernotdeliveredTable2ConstraintsetCONDforcustomerorderchanged2CONDSemanticofConstraintSetDefinitiontoSemanticofConstraintSetDeliveredtocustomer,thenordercan