Efficient Refinement Checking in VCCEfficient检查和VCCEfficient

Efficient Refinement Checking in VCCEfficient检查和VCCEfficient

ID:39065775

大小:1.16 MB

页数:17页

时间:2019-06-24

Efficient Refinement Checking in VCCEfficient检查和VCCEfficient_第1页
Efficient Refinement Checking in VCCEfficient检查和VCCEfficient_第2页
Efficient Refinement Checking in VCCEfficient检查和VCCEfficient_第3页
Efficient Refinement Checking in VCCEfficient检查和VCCEfficient_第4页
Efficient Refinement Checking in VCCEfficient检查和VCCEfficient_第5页
资源描述:

《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

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。