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

淮北师范大学 2015届学士学位论文

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

学 院 计算机科学与技术 专 业 计算机科学与技术 研 究 方 向 嵌入式软件的形式化方法 学 生 姓 名 王超龙 学 号 20111201039 指导教师姓名 马艳芳 指导教师职称 副教授

2015 年 4 月 22 日

作 者 声 明

我郑重承诺：本人恪守学术道德，崇尚严谨学风。所成交的学位论文，是本人在教师的的指导下，独立进行研究工作所取得的结果。初吻中明确注明和引用的内容外，本论文不包含任何他人已发表或撰写的内容。论文为本人亲自撰写，并对所写内容负责。

作者签名：

2015年4月20日

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

摘 要

随着嵌入式应用的快速发展,嵌入式实时软件业已成为软件测试领域的一个研究热点。由于嵌入式软件本事的确定性、并发性、实时性，对此类系统进行形式化建模具有很大的挑战性；进一步说，验证嵌入式系统是否满足可靠性、安全性、活性等关键属性具有十分重要的意义。现有的研究多由于形式化的方法。形式化方法对问题的描述较深刻、严谨,但它要求开发人员具备很好的数学基础和数理逻辑方面的知识,因而难以掌握。

UML是工业上软件建模事实上的标准语言，它的多种视图为嵌入式系统的结构、行为建模提供的便利；组件图是工业上普遍采用的一种描述嵌入式系统静态结构的可视化方法，它将复杂的系统划分为多个组件并且描述了这些组件之间的交互依赖；此外，还可以使用体系结构描述语言对其进行形式化描述，本文针对在嵌入式实时软件测试中形式化方法的一些局限性,提出一种基于UML状态图的测试用例生成方法。为了弥补UML状态图在描述实时系统上的不足,给出了一个状态图的实时扩展方案。我们在他人的状态空间划分法的基础上,提出了迁移等价类和测试树的概念,讨论了通过测试树生成测试用例的方法,随后结合一个自动售货机的例子说明了该方法的使用过程。最后介绍了原型工具RTTC的设计与实现嵌入式软件是复杂的反应系统，其主要特点是持续与外部环境进行交互、运行通常没有终止状态。

关键词 嵌入式软件 形式化方法 UML 状态图

As the formalization ways of embedded software

Abstract

With the rapid development of embedded application, embedded real-time software has become a research hotspot in the field of software testing. Because of the skill of certainty, concurrency, real-time embedded software, to the formal modeling was challenging the system; Further, verify whether the embedded system to meet key properties such as reliability, security, activity has the very vital significance. Due to the existing research and the formal method. Formalism description of the problem is profound, rigorous, but it requires developers to have very good mathematical foundation and knowledge of mathematical logic, so difficult to master. The DE facto standard software modeling language UML is industry, its variety of view for the structure of embedded system, behavior modeling is convenient; Component diagram is widely used in industry a describes the static structure of the embedded system visualization method, it will be a complex system is divided into multiple components and to describe the interaction between these components rely on; In addition, you can also use the architecture description language for its formal description, this paper in the embedded real-time software testing some of the limitations of formal methods, put forward a kind of test case generation method based on UML state diagram. To make up for the UML state chart to describe the lack of real-time systems, a state diagram of real-time extension scheme is given. We in other people's, on the

basis of state space partition method, puts forward the concept of migration equivalence class and test, discussed the method to test the tree to generate test cases through, then combined with a vending machine example illustrates the process using this method. Finally this paper introduces the design and implementation of a prototype tool RTTC embedded software is a complex reaction system, its main characteristic is continue to interact with the external environment, run, there is usually no termination status.

Keyword：Embedded software formalization method of UML state diagram

目 录

摘要??????????????????????????????????????.1 Abstract?????????????????????????????????????2-3 第一章 诸论???????????????????????????????????6-8 1．1 研究背景及意义???????????????????????????????6 1．2 国内外的研究现状??????????????????????????????7 1．3 相关技术与背景???????????????????????????????7 1．4 本文的主要工作和结构????????????????????????????.8 第二章 嵌入式软件????????????????????????????????.8

2.1嵌入式系统????????????????????????????.8 2.2软件的背景????????????????????????????.8 2.3嵌入式软件的发展历程???????????????????????.8 2.4常用的分类????????????????????????????.9 第三章 软件的形式化方法????????????????????????9 3.1情况??????????????????????????????...9 3.2发展过程?????????????????????????????.10 3.3定义???????????????????????????????.10 3.4研究内容?????????????????????????????.11 第四章 UML状态图????????????????????????????12 4.1 简介???????????????????????????????.12 4.2 历史???????????????????????????????.13

4.3 主要内容?????????????????????????????.14 4.4 分类???????????????????????????????.15 4.5 应用领域?????????????????????????????.16 4.6 发展历史?????????????????????????????.17 4.7 应用???????????????????????????????.18 第五章 总结与展望????????????????????????????19 5.1 总结???????????????????????????????.19 5.2 展望???????????????????????????????.19 参考文献 致谢

第一章 绪论

1.1研究背景与意义

近年来随着嵌入式系统硬件性能的不断提高,嵌入式系统中软件的规模和复杂性也不断增加,软件对整个系统的影响逐渐占据了统治地位,从而使得嵌入式软件设计以及可靠性保障变得越来越困难。传统的嵌入式软件设计方法已经逐渐难以满足现代嵌入式软件设计的高可靠性需求,必须结合主流软件工程中处理复杂软件系统所采用的理论、技术与方法,如构件化设计、模型驱动架构、形式化规约与验证等。目前,模型驱动的嵌入式软件设计方法已经成为嵌入式计算领域中的研究热点。 形式化方法是以数学为基础的用以对系统进行规约、设计和验证的语言、技术和工具的总称。对于具有高可靠性需求的嵌入式软件系统而言,建立有效的形式化验证技术具有非常重要的意义。

因此,在嵌入式软件需求规约阶段引入形式化方法,并根据需求规约生成保留形式化语义的软件体系结构模型,可以极大提高嵌入式软件设计的可靠性。

嵌入式系统在人类生活中发挥着重要的作用，系统中软件的比重越来越大，对嵌入式软件进行测试是保证其质量的一种重要手段之一。本文从嵌入式软件测试特点出发，着重探讨嵌入式软件的测试方法和测试策略。这些对于提高和改善嵌入式软件的质量具有指导意义。

1.2 国内外研究现状

目前，大多数计算机系统都属于嵌入式系统。嵌入式系统通常是安全攸关系统和实时系统，前者意味着系统失败会导致灾难性的后果，后者意味着他们的正确行为不仅依赖着逻辑计算，也依赖着结果产生的时间。因此，采取形式化的方法对嵌入式系统进行建模和验证，不断提高系统的正确性和可靠性已经成为国内外许多学者的研究方向。

L.A.C等提出了一种基于Petri网的嵌入式系统建模和研究方法。该方法引入了PRES+捕获嵌入式系统的重要特征，使用CTL或TCTL公式描述系统的关键属性，最后采用模型检验工具自动化验证是否系统模型满足关键性质。F.了一种可配置嵌入式系统的建模和验证方法。该方法使用可配置离散事

百度搜索“77cn”或“免费范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，免费范文网，提供经典小说教育文库王超龙 嵌入式软件的形式化方法研究在线全文阅读。