资源描述：
《Compositional Verification of Middleware-Based Software Architecture Description》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、CompositionalVerificationofMiddleware-BasedSoftwareArchitectureDescriptionsMauroCaporuscio,PaolaInverardi,PatrizioPelliccioneDipartimentodiInformaticaUniversit`adell’AquilaI-67010L’Aquila,Italy{caporusc,inverard,pellicci}@di.univaq.itAbstractthestateexplosionproblem.Asremarked
2、byGeraldHolz-mannin[22]nopaperwaspublishedonreachabilityanal-Inthispaperwepresentacompositionalreasoningysistechniqueswithoutaseriousdiscussionofthisprob-toverifymiddleware-basedsoftwarearchitecturedescrip-lem.Stateexplosionoccurseitherinsystemscomposedoftions.Weconsideranowa
3、daystypicalsoftwaresystemde-(nottoo)manyinteractingcomponents,orinsystemswherevelopment,namelythedevelopmentofasoftwareapplica-datastructuresassumemanydifferentvalues.ThenumbertionAonamiddlewareM.Ourgoalistoefficientlyin-ofglobalstateseasilybecomesenormousandintractable.tegrat
4、everificationtechniques,likemodelchecking,intheTosolvethisproblem,manymethodshavebeendevel-softwarelifecycleinordertoimprovetheoverallsoftwareopedbyexploitingdifferentapproaches[10].Theycanbequality.Theapproachexploitsthestructureimposedonthelogicallyclassifiedintotwodisjointse
5、ts.Thefirstset,thatsystembythesoftwarearchitectureinordertodevelopanwecallInternalMethods,considersalgorithmsandtech-assume-guaranteemethodologytoreducepropertiesverifi-niquesusedinternallytothemodelcheckerinordertoef-cationfromglobaltolocal.Weapplythemethodologyonaficientlyrepr
6、esenttransitionrelationsbetweenconcurrentnon-trivialcasestudynamelythedevelopmentofaGnutellaprocesses,suchasBinaryDecisionDiagrams[3](usedforsystemontopoftheSIENAevent-notificationmiddleware.synchronousprocesses)andPartialOrderReduction[27]techniques(usedforasynchronousprocess
7、es).Thesecondset,thatwecallExternalMethodsincludes1.Introductiontechniquesthatoperateontheinputofthemodelchecker(models),andcanbeusedinconjunctionwithInternalInthispaperwepresentacompositionalreasoningtoMethods.InthissetthereareAbstraction[9],Symme-verifymiddleware-basedSoftw
8、areArchitecture(SA)de-try[14]andCompositionalReasoning[16,33].Inpart
