资源描述：
《Efficient Refinement Checking in VCCEfficient检查和VCCEfficient》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、EfficientRefinementCheckinginVCCSumeshDivakaran1(B),DeepakD’Souza1,andNigamanthSridhar21IndianInstituteofScience,Bangalore,India{sumeshd,deepakd}@csa.iisc.ernet.in2ClevelandStateUniversity,Cleveland,OH,USAn.sridhar1@csuohio.eduAbstract.Weproposeamethodologyfo
2、rcarryingoutrefinementproofsacrossdeclarativeabstractmodelsandconcreteimplementationsinC,usingtheVCCverificationtool.Themainideaistofirstperformasystem-atictranslationfromthetop-levelabstractmodeltoaghostimplementa-tioninVCC.Subsequentrefinementproofsbetweensu
3、ccessivelyrefinedabstractmodelsandbetweenabstractandconcreteimplementationsarecarriedoutinVCC.WeproposeanefficienttechniquetocarryouttheserefinementchecksinVCC.WeillustrateourmethodologywithacasestudyinwhichweverifyasimplifiedCimplementationofanRTOSscheduler,wi
4、threspecttoitsabstractZspecification.Overall,ourmethodologyleadstoefficientandautomaticrefinementproofsforcomplexsystemsthatwouldtypicallybebeyondthecapabilityoftoolssuchasZ/EvesorRodin.1IntroductionRefinement-basedtechniquesareawell-developedapproachtoprovingf
5、unc-tionalcorrectnessofsoftwaresystems.Inacorrect-by-constructionapproachusingstep-wiserefinement,onebeginswithanabstractspecificationofthesys-tem’sfunctionality,sayM1,andsuccessivelyrefinesitviasomeintermediatemodels,toaconcreteimplementation,sayP2inanimpera
6、tivelanguage.Simi-larly,inapost-factoproofofcorrectness,onebeginswithaconcreteimplemen-tationP2,specifiesitsfunctionalityabstractlyinM1,andcomesupwiththeintermediatemodelsbysimultaneouslyrefiningM1towardsP2andabstractingP2towardsM1.ThisisdepictedinFig.1(a).W
7、enotethatitisconvenienttohaveM1specifiedinanabstractmodellinglanguagesuchasZ[16]orEvent-B[1],sincethisgivesusaconciseyetreadable,andmathematicallyprecisespecifi-cationofthesystem’sbehaviour,whichservesasaspecificationoffunctionalbehaviourforusersandclientsoft
8、hesystem.Refinement-basedproofsoffunctionalcorrectnesshaveseveraladvantagesoveranapproachofdirectlyphrasingandprovingpreandpostconditionsonmethods.Tobeginwith,refinement-basedapproacheshelptobreakdownasser-tion
