资源描述：
《王超龙 嵌入式软件形式化方法研究分析》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。
1、...页眉淮北师范大学2015届学士学位论文嵌入式软件的形式化方法研究学院计算机科学与技术专业计算机科学与技术研究方向嵌入式软件的形式化方法学生姓名王超龙学号20111201039指导教师姓名马艳芳指导教师职称副教授2015年4月22日作者声明....页脚...页眉我郑重承诺：本人恪守学术道德，崇尚严谨学风。所成交的学位论文，是本人在教师的的指导下，独立进行研究工作所取得的结果。初吻中明确注明和引用的内容外，本论文不包含任何他人已发表或撰写的内容。论文为本人亲自撰写，并对所写内容负责。作者签名：2015年4月20日嵌入式软件的形式化方法研究摘要随着嵌
2、入式应用的快速发展,嵌入式实时软件业已成为软件测试领域的一个研究热点。由于嵌入式软件本事的确定性、并发性、实时性，对此类系统进行形式化建模具有很大的挑战性；进一步说，验证嵌入式系统是否满足可靠性、安全性、活性等关键属性具有十分重要的意义。现有的研究多由于形式化的方法。形式化方法对问题的描述较深刻、严谨,但它要求开发人员具备很好的数学基础和数理逻辑方面的知识,因而难以掌握。UML是工业上软件建模事实上的标准语言，它的多种视图为嵌入式系统的结构、行为建模提供的便利；组件图是工业上普遍采用的一种描述嵌入式系统静态结构的可视化方法，它将复杂的系统划分为多个组
3、件并且描述了这些组件之间的交互依赖；此外，还可以使用体系结构描述语言对其进行形式化描述，本文针对在嵌入式实时软件测试中形式化方法的一些局限性,提出一种基于UML状态图的测试用例生成方法。为了弥补UML状态图在描述实时系统上的不足,给出了一个状态图的实时扩展方案。我们在他人的状态空间划分法的基础上,提出了迁移等价类和测试树的概念,讨论了通过测试树生成测试用例的方法,随后结合一个自动售货机的例子说明了该方法的使用过程。最后介绍了原型工具RTTC的设计与实现嵌入式软件是复杂的反应系统，其主要特点是持续与外部环境进行交互、运行通常没有终止状态。关键词嵌入式软
4、件形式化方法UML状态图....页脚...页眉AstheformalizationwaysofembeddedsoftwareAbstractWiththerapiddevelopmentofembeddedapplication,embeddedreal-timesoftwarehasbecomearesearchhotspotinthefieldofsoftwaretesting.Becauseoftheskillofcertainty,concurrency,real-timeembeddedsoftware,totheformalmodeli
5、ngwaschallengingthesystem;Further,verifywhethertheembeddedsystemtomeetkeypropertiessuchasreliability,security,activityhastheveryvitalsignificance.Duetotheexistingresearchandtheformalmethod.Formalismdescriptionoftheproblemisprofound,rigorous,butitrequiresdeveloperstohaveverygood
6、mathematicalfoundationandknowledgeofmathematicallogic,sodifficulttomaster.TheDEfactostandardsoftwaremodelinglanguageUMLisindustry,itsvarietyofviewforthestructureofembeddedsystem,behaviormodelingisconvenient;Componentdiagramiswidelyusedinindustryadescribesthestaticstructureofthe
7、embeddedsystemvisualizationmethod,itwillbeacomplexsystemisdividedintomultiplecomponentsandtodescribetheinteractionbetweenthesecomponentsrelyon;Inaddition,youcanalsousethearchitecturedescriptionlanguageforitsformaldescription,thispaperintheembeddedreal-timesoftwaretestingsomeoft
8、helimitationsofformalmethods,putforwardakindoftestcase
