王超龙 嵌入式软件的形式化方法研究

淮北师范大学2015届学士学位论文嵌入式软件的形式化方法研究学院计算机科学与技术专业计算机科学与技术研究方向嵌入式软件的形式化方法学生姓名王超龙学号20111201039指导教师姓名马艳芳指导教师职称副教授2015年4月22日作者声明我郑重承诺：本人恪守学术道德，崇尚严谨学风。所成交的学位论文，是本人在教师的的指导下，独立进行研究工作所取得的结果。初吻中明确注明和引用的内容外，本论文不包含任何他人已发表或撰写的内容。论文为本人亲自撰写，并对所写内容负责。作者签名：2015年4月20日嵌入式软件的形式化方法研究摘要随着嵌入式应用的快速发展,嵌入式实时软件业已成为软件测试领域的一个研究热点。由于嵌入式软件本事的确定性、并发性、实时性，对此类系统进行形式化建模具有很大的挑战性；进一步说，验证嵌入式系统是否满足可靠性、安全性、活性等关键属性具有十分重要的意义。现有的研究多由于形式化的方法。形式化方法对问题的描述较深刻、严谨,但它要求开发人员具备很好的数学基础和数理逻辑方面的知识,因而难以掌握。UML是工业上软件建模事实上的标准语言，它的多种视图为嵌入式系统的结构、行为建模提供的便利；组件图是工业上普遍采用的一种描述嵌入式系统静态结构的可视化方法，它将复杂的系统划分为多个组件并且描述了这些组件之间的交互依赖；此外，还可以使用体系结构描述语言对其进行形式化描述，本文针对在嵌入式实时软件测试中形式化方法的一些局限性,提出一种基于UML状态图的测试用例生成方法。为了弥补UML状态图在描述实时系统上的不足,给出了一个状态图的实时扩展方案。我们在他人的状态空间划分法的基础上,提出了迁移等价类和测试树的概念,讨论了通过测试树生成测试用例的方法,随后结合一个自动售货机的例子说明了该方法的使用过程。最后介绍了原型工具RTTC的设计与实现嵌入式软件是复杂的反应系统，其主要特点是持续与外部环境进行交互、运行通常没有终止状态。关键词嵌入式软件形式化方法UML状态图AstheformalizationwaysofembeddedsoftwareAbstractWiththerapiddevelopmentofembeddedapplication,embeddedreal-timesoftwarehasbecomearesearchhotspotinthefieldofsoftwaretesting.Becauseoftheskillofcertainty,concurrency,real-timeembeddedsoftware,totheformalmodelingwaschallengingthesystem;Further,verifywhethertheembeddedsystemtomeetkeypropertiessuchasreliability,security,activityhastheveryvitalsignificance.Duetotheexistingresearchandtheformalmethod.Formalismdescriptionoftheproblemisprofound,rigorous,butitrequiresdeveloperstohaveverygoodmathematicalfoundationandknowledgeofmathematicallogic,sodifficulttomaster.TheDEfactostandardsoftwaremodelinglanguageUMLisindustry,itsvarietyofviewforthestructureofembeddedsystem,behaviormodelingisconvenient;Componentdiagramiswidelyusedinindustryadescribesthestaticstructureoftheembeddedsystemvisualizationmethod,itwillbeacomplexsystemisdividedintomultiplecomponentsandtodescribetheinteractionbetweenthesecomponentsrelyon;Inaddition,youcanalsousethearchitecturedescriptionlanguageforitsformaldescription,thispaperintheembeddedreal-timesoftwaretestingsomeofthelimitationsofformalmethods,putforwardakindoftestcasegenerationmethodbasedonUMLstatediagram.TomakeupfortheUMLstatecharttodescribethelackofreal-timesystems,astatediagramofreal-timeextensionschemeisgiven.Weinotherpeople's,onthebasisofstatespacepartitionmethod,putsforwardtheconceptofmigrationequivalenceclassandtest,discussedthemethodtotestthetreetogeneratetestcasesthrough,thencombinedwithavendingmachineexampleillustratestheprocessusingthismethod.FinallythispaperintroducesthedesignandimplementationofaprototypetoolRTTCembeddedsoftwareisacomplexreactionsystem,itsmaincharacteristiciscontinuetointeractwiththeexternalenvironment,run,thereisusuallynoterminationstatus.Keyword：EmbeddedsoftwareformalizationmethodofUMLstatediagram目录摘要…………………………………………………………………………………………………….1Abstract…………………………………………………………………………………………………2-3第一章诸论……………………………………………………………………………………………6-81．1研究背景及意义…………………………………………………………………………………61．2国内外的研究现状………………………………………………………………………………71．3相关技术与背景…………………………………………………………………………………71．4本文的主要工作和结构………………………………………………………………………….8第二章嵌入式软件…………………………………………………………………………………….82.1嵌入式系统………………………………………………………………………….82.2软件的背景………………………………………………………………………….82.3嵌入式软件的发展历程…………………………………………………………….82.4常用的分类………………………………………………………………………….9第三章软件的形式化方法………………………………………………………………93.1情况………………………………………………………………………………...93.2发展过程…………………………………………………………………………….103.3定义………………………………………………………………………………….103.4研究内容…………………………………………………………………………….11第四章UML状态图…………………………………………………………………………124.1简介………………………………………………………………………………….124.2历史………………………………………………………………………………….134.3主要内容…………………………………………………………………………….144.4分类………………………………………………………………………………….154.5应用领域…………………………………………………………………………….164.6发展历史…………………………………………………………………………….174.7应用………………………………………………………………………………….18第五章总结与展望…………………………………………………………………………195.1总结………………………………………………………………………………….195.2展望………………………………………………………………………………….19参考文献致谢第一章绪论1.1研究背景与意义近年来随着嵌入式系统硬件性能的不断提高,嵌入式系统中软件的规模和复杂性也不断增加,软件对整个系统的影响逐渐占据了统治地位,从而使得嵌入式软件设计以及可靠性保障变得越来越困难。传统的嵌入式软件设计方法已经逐渐难以满足现代嵌入式软件设计的高可靠性需求,必须结合主流软件工程中处理复杂软件系统所采用的理论、技术与方法,如构件化设计、模型驱动架构、形式化规约与验证等。目前,模型驱动的嵌入式软件设计方法已经成为嵌入式计算领域中的研究热点。形式化方法是以数学为基础的用以对系统进行规约、设计和验证的语言、技术和工具的总称。对于具有高可靠性需求的嵌入式软件系统而言,建立有效的形式化验证技术具有非常重要的意义。因此,在嵌入式软件需求规约阶段引入形式化方法,并根据需求规约生成保留形式化语义的软件体系结构模型,可以极大提高嵌入式软件设计的可靠性。嵌入式系统在人类生活中发挥着重要的作用，系统中软件的比重越来越大，对嵌入式软件进行测试是保证其质量的一种重要手段之一。本文从嵌入式软件测试特点出发，着重探讨嵌入式软件的测试方法和测试策略。这些对于提高和改善嵌入式软件的质量具有指导意义。1.2国内外研究现状目前，大多数计算机系统都属于嵌入式系统。嵌入式系统通常是安全攸关系统和实时系统，前者意味着系统失败会导致灾难性的后果，后者意味着他们的正确行为不仅依赖着逻辑计算，也依赖着结果产生的时间。因此，采取形式化的方法对嵌入式系统进行建模和验证，不断提高系统的正确性和可靠性已经成为国内外许多学者的研究方向。L.A.C等提出了一种基于Petri网的嵌入式系统建模和研究方法。该方法引入了PRES+捕获嵌入式系统的重要特征，使用CTL或TCTL公式描述系统的关键属性，最后采用模型检验工具自动化验证是否系统模型满足关键性质。F.了一种可配置嵌入式系统的建模和验证方法。该方法使用可配置离散事件规约系统（c计算模型对复杂嵌入式系统建模，然后将模型转换为UPPAL模型检验工具的输入语言进行验证，并提出了模型到语言的自动化转换算法，最后通过复杂的汽车应用系统验证了模型的有效性。R.A提出了一种基于组建建模与验证自适应嵌入式系统的新方法。基于组建建模方法抽象组建的合成为层次组件，从而将大量的组建配置精化为少量的层次配置，大大降低了系统设计的复杂性。此外，为保证组件的良好定义，提出了一个形式化计算模型用于自动化验证自适应嵌入式系统的关键需求。杨年华等提出了一种基于带抑制弧的时延着色Pert网的实时嵌入式系统建模和验证方法，并通过案例验证了该方法的可用性和实用性。郭军等结合了双变迁Petri网和面向对象设计方法对复杂嵌入式系统建模，并通过实例仿真证明了设计方法的可行性和实用性。以上各种建模方法都有效的实现了模型的形式化验证，但都没有考虑系统中横切关注点的建模问题，导致了模型的复杂性和低效性。将来面向方面技术应用于嵌入式系统的建模中，可有效的分离嵌入式