基于模型的实时系统形式化验证方法研究与实现

《基于模型的实时系统形式化验证方法研究与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、硕±学位论文题目；基于模型的实时系统形式化验证方法研究与实现研究生冯博洋专业计算机技术指导教师方景龙研究员完成目期２０１６年３月杭州电子科技大学硕士学位论文基于模型的实时系统形式化验证方法研究与实现研究生：冯博洋指导教师：方景龙研究员2016年3月DissertationSubmittedtoHangzhouDianziUniversityfortheDegreeofMasterResearchandimplementionofmodelbasedreal-timesystemformalizationvalidationC

2、andidate:BoyangFengSupervisor:Prof.JinglongFangMarch,2016巧州电子科技大学学位论文原创性声明和使用授权说明原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进斤研究工作所取得的成果。除文中已经注明引用的肉容外，本论文不含任何其他个人或集体已经发表或撰写过的作品或成果。对本文的研巧做出重要贡献的个人和集体，均已在文中Ｗ明确方式标明。一申请学位论文与资料若有不实么处，本人承担切相关责任。论文作者签名曰期：文（？／（年３月ｙ曰学位论文使用授权说明，即本人完

3、全了解杭州电子科技大学关于保留和使用学位论文的规定：研究生在校攻读学位期间论文工作的知识产权单位属杭州电子科技大学。本人保证毕，发表论文或使用论文工作成果时署名单位仍然为杭州电子科技大学业离校后。学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可Ｗ公布论文的全部或部分内容，可Ｗ允许采用影印、缩印或其它复制手段保存论文。（保密论文在解密后遵守此规定）＾６论文作者签名曰期：２年３月＾曰指导教师签名日期：山年言月Ｓ日杭州电子科技大学硕士学位论文摘要随着计算机技术的发展，尤其是实时系统在各个领域的渗透，软件工程领域中对实时系统的功能

4、行为、资源利用状况、能量消耗等特性的认识越来越深入，如何才能够在系统模型设计阶段保证其可靠性已经成为领域内关注的热点。在系统开发的过程中，UML已经成为设计人员广泛使用的建模语言，尤其是计时图拥有出色的时间因素表现能力是实时系统建模的不二选择。由于UML是一种半形式化的建模语言，不能直接在其基础上进行模型验证，而时间自动机模型是一种完全形式化的语言，UPPAAL是基于时间自动机的验证工具，可以对实时系统进行实时功能验证。因此本文以计时图模型作为实时系统的建模模型，通过模型转换算法将其转换为UPPAAL中的时间自动机验证模型。本文首先介绍了实时系统形式化验证的相关

5、理论与技术，给出了UML计时图和时间自动机的形式化描述，改进现有的模型转换方法，将计时图模型转换为时间自动机。然后利用转换后的时间自动机进行功能验证，并对时间自动机做了进一步的扩展，给出了资源时间自动机、能耗时间自动机的形式化定义，在其基础上进行资源、能耗的非功能验证。最后根据本文研究的形式化验证方法，实现了原型工具T-RTSMD，并在两个不同应用领域的实例上验证了该方法的有效性。关键词：计时图，时间自动机，实时系统，形式化，验证I杭州电子科技大学硕士学位论文ABSTRACTWiththedevelopmentofcomputertechnology,espec

6、iallytheapplicationofreal-timesysteminvariousareas,thefeatures,whichincludefunctionbehavior,theresourceutilizationandenergyconsumptionofreal-timesysteminthefieldofsoftwareengineering,aregettingmoreandmorein-depthunderstanding.Howtoensurethereliabilityofareal-timesystemduringitsmodeld

7、esignphasebecomesafocusofthefield.Duringtheprocessofsystemdevelopment,UnifiedModelingLanguage(UML)haswidelyusedbythedesigners.Anditbecomesthebestchoiceformodelingthereal-timesystemduetotheexcellentperformanceofthetimediagramintimefactor.However,UMLisahalf-formalizedlanguagewhichcanno

8、tbeusedtoach