淮北师范大学
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.了一种可配置嵌入式系统的建模和验证方法。该方法使用可配置离散事
件规约系统（c计算模型对复杂嵌入式系统建模，然后将模型转换为UPPAL模型检验工具的输入语言进行验证，并提出了模型到语言的自动化转换算法，最后通过复杂的汽车应用系统验证了模型的有效性。R.A提出了一种基于组建建模与验证自适应嵌入式系统的新方法。基于组建建模方法抽象组建的合成为层次组件，从而将大量的组建配置精化为少量的层次配置，大大降低了系统设计的复杂性。此外，为保证组件的良好定义，提出了一个形式化计算模型用于自动化验证自适应嵌入式系统的关键需求。杨年华等提出了一种基于带抑制弧的时延着色Pert网的实时嵌入式系统建模和验证方法，并通过案例验证了该方法的可用性和实用性。郭军等结合了双变迁Petri网和面向对象设计方法对复杂嵌入式系统建模，并通过实例仿真证明了设计方法的可行性和实用性。以上各种建模方法都有效的实现了模型的形式化验证，但都没有考虑系统中横切关注点的建模问题，导致了模型的复杂性和低效性。
将来面向方面技术应用于嵌入式系统的建模中，可有效的分离嵌入式系统的核心关注点与横切关注点，不仅有助于提高模型的模块化程度，也有助于模型的形式化验证，很多学者都在此领域探索。
C.D等阐述了如何使用Theme/UML，用于支持基于Theme/UML的模块化设计，并支持合成模型和源代码的自动转化。N.M等提出了一种基于面向方向建模方法构建嵌入式实时系统的应用。该方法使用MARTE术语描述实时约束，并设计阶段编制实时约束到标准应用程序中，从而转换标准应用程序为实时程序，该方法根据设定的规则修改标准应用程序的结构和行为。张立臣提出了一种实时系统的面向方面形式化规约方法。该方法通过将实时系统分离为不同方面，然后单独的实现每方面，最后通过隐式编制的方法将这些方面植入系统中。
分析上述研究成果可以发现，对UML进行面向方面扩展构建嵌入式系统模型，使用时态逻辑描述系统的关键属性，最后使用模型检测的方法对模型进行分析和验证，是一种最直接，最自然的方法。由于有限状态机无法描述复杂嵌入式系统中的并发与层次关系，因此，本文提出一种基于State的复杂嵌入式系统建模方法，对UML的用例图，组件图和States进行面向方向扩展，从而实现复杂需求到系统实现的平滑过渡。
1.3 相关技术背景
UML是一种面向对象软件的标准化建模语言。UML因其简单、统一的特点，而且能表达软件设计中的动态和静态信息，目前已成为可视化建模语言的工业标准。在软件无线电系统的开发过程中，统一建模语言可以在整个设计周期中使用，帮助设计者缩短设计时间，减少改进的成本，使软硬件分割最优。
UML还具有以下分类：用例图、静态图、行为图、交互图、实现图
对于UML的详细介绍，我们下文还会继续讲解。
嵌入式软件就是嵌入在硬件中的操作系统和开发工具软件，它在产业中的关联关系体现为：芯片设计制造→嵌入式系统→嵌入式电子设备开发、制造。
嵌入式系统是指用于执行独立功能的专用计算机系统。
形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。
1.4 论文的主要功能和结构
本文主要针对嵌入式软件进行研究，嵌入式软件在现在社会的各个方面具有广泛应用，我们首先介绍嵌入式软件—在介绍形式化方法--在对嵌入式软件进行需求分析—再介绍嵌入式软件架构设计—实施软件分析方法—嵌入式软件的可靠性设计—嵌入式软件的开发环境。
具体内容如下：
（1）嵌入式软件
主要是介绍什么的嵌入式软件，通过对嵌入式软件的了解以及它的重要性，进一步的认识到对嵌入式软件进行研究的必要性。
（2）形式化方法
什么是形式化方法，以及形式化方法在软件设计方面的重要性。形式化方法以其本身的逻辑性、严谨性，既可以在事前预判起到参考作用，又可以在软件开发的过程中起到修正作用。
（3）嵌入式软件的需求分析
我们在设计软件时，要对其进行市场调查和需求分析，即包括传统的需求问题有包括现在的各种情况，我们在软件设计之间对嵌入式软件的进行详细的定义和分析。
（4）嵌入式软件的架构设计
架构设计是从系统的角度，对整个系统高层次的设计。嵌入式系统的软件和硬件是相互结合的，是对整体进行设计的因此要进行软件的架构设计。
（5）嵌入式软件的可靠性设计
所谓的可靠性设计是指产品在规定条件下和规定时间内，完成规定功能的能力。
论文结构
本文是针对嵌入式软件进行研究的，所以可以从以下几个点出发，
第一章本文提出了本文的研究背景、研究意义以及研究内容。
第二章本文介绍了什么是嵌入式软件以及它的一些性质。
第三章本文介绍了什么是形式化方法以及常用的软件开发方法。
第四章本文对UML状态图进行讲解和说明，从而得出它在嵌入式软件开发方面的用途。第五章本章对本文的研究内容进行总结，同时指出本文的不足之处，并对下一步的工作和未来研究方向进行展望。
第二章嵌入式软件
引言：嵌入式软件是实现嵌入式计算机系统功能的软件。嵌入式软件发展的非常快，而嵌入式软件发展的更快。嵌入式软件就像生物的发展一样，有单细胞生物想多细胞生物，一直到智能生物人类，在这个过程中，嵌入式软件越来越复杂，嵌入式软件就是嵌入在硬件中的操作系统和开发工具软件，它在产业中的关联关系体现为：芯片设计制造→嵌入式系统→嵌入式电子设备开发、制造。
2.1嵌入式系统
定义嵌入式系统是指用于执行独立功能的系统。它由包括微处理器、定时器、微控制器、存储器、传感器等一系列微电子芯片与器件，和嵌入在存储器中的微型操作系统、控制应用软件组成，共同实现诸如实时控制、监视、管理、移动计算、数据处理等各种自动化处理任务、嵌入式系统以应用为中心，以微电子技术、控制技术、计算机技术和通讯技术为基础，强调硬件软件的协同性与整合性，软件与硬件可剪裁，以此满足系统对功能、成本、体积和功耗等要求。
最简单的嵌入式系统仅有执行单一功能的控制能力，比如说单片机的应用，在唯一的ROM 中仅有实现单一功能控制程序，无微型操作系统。复杂的嵌入式系统，例如个人数字电脑（PDA）、手持电脑（HPC）等，具有与PC几乎一样的功能。实质上与PC的区
别仅仅是将微型操作系统与应用软件嵌入在ROM、RAM 和/或FLASH存储器中，而不是存贮于磁盘等载体中。很多复杂的嵌入式系统又是由若干个小型嵌入式系统组成的。2.2背景
近些年来，随着以计算机技术，通讯技术为主的信息技术的快速发展和Internet 的广泛应用，传统的控制学科正在发生变革，出现了许多新的生长点。伴随而来的一个现象是控制专业的相当多的学生在毕业后进入了计算机，通讯行业，以致有人说学控制没有用，自动化专业可以取消了。这些情况的出现使我们控制教育工作者反复思考，传统的控制应如何拓宽它的领域？控制专业应该教什么才使学生感到有用？
2.3发展历程
第一阶段：早期的嵌入式程序设计方法，通常是采用“硬件优先”原则。即在只粗略估计软件任务需求的情况下，首先进行硬件设计与实现。然后，在此硬件平台之上，再进行软件设计。因而很难达到充分利用硬件材料资源，取得最佳性能的效果。同时，一旦在测试时发现问题，需要对设计进行修改时，整个设计流程将重新进行，对成本和设计周期的影响很大。这种传统的设计方法只能改善硬件/软件各自的性能，在有限的设计空间不可能对系统做出较好的性能综合优化，在很大程度上依赖于设计者的经验和反复实验。
第二阶段：90年代以来随着电子系统功能的日益强大和微型化，系统设计所涉及的问题越来越多，难度也越来越大。同时硬件和软件也不再是截然分开的两个概念，而是紧密结合、相互影响的。因而出现了软硬件协同设计方法，即使用统一的方法和工具对软硬件，协调设计软硬件体系结构，以最大限度地挖掘系统软硬件能力，避免由于独立设计软硬件体系结构而带来的种种弊病，得到高性能低代价的优化设计方案。
2.4分类
流行的嵌入式操作系统可以分为两类：
一类是从运行在个人电脑上的操作系统向下移植到嵌入式系统中，形成的嵌入式操作系统，Windows CE及其新版本，SUN公司的Java，朗讯科技的Inferno，嵌入式Linux 等。这类系统经过个人电脑或高性能的产品的长期运行考验，技术日趋成熟，其相关的标准开发方式已被用户普遍接受，同时积累了丰富的开发工具和应用软件资源。
另一类是实时操作系统，如系统软件公司的QNX，ATI 的Nucleus，中科院凯思集团的Hop操作系统，这类产品在操作系统的结构和实现上都针对所面向的应用领域，对实时性高可靠性等进行了精巧的设计，而且提供了独立而完备的系统开发和测试工具，较多地应用在军用产品和工业控制等领域中。
Linux 是90年代以来逐渐成熟的一个开放源代码操作系统。PC机上的Linux 版本在全球数以百万计爱好者的合力开发下，得到了非常迅速的发展。90 年代相继推出，在嵌入式领域得到了广泛的关注，它拥有大批的程序员和现成的应用程序，是我们研究开发工作的宝贵资源。
第三章软件的嵌入式方法
形式化方法英文的名称是formal methods。在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包含概念彼此间的联结,推理中则是各个命题之间的联结,抽取出它们共同的形式结构;再引入表达形式结构的符号语言,用符号与符号之间的联系表达命题或推理的形式结构。例如,把全称肯定命题,用符号形式化为“SAP”;把联言命题、假命题分别形式化为:“p∧q、“p→q”。又例如:一个具体的假言联言推理“如果这种金属是纯铝,那么它的物理性质必与纯铝相同;如果这种金属是纯铝,那么它的化学性质必与纯铝相同;但这种金属的物理性质和化学性质与纯铝不相同;所以,它不是纯铝。”这个推理的形式结构是:“如果p,则q;如果p,则r;非q且非r;所以非p。”可进而形式化为下列公式:((p→q)∧(p→r)∧┐q∧┐r→┐p。
3.1基本信息
在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计的可靠性和安全性。但是，由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。
形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数，人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应的逻辑规则,使各种理论体系更加严密。同时也能正确地训练思维、提高思维的抽象能力。
3.2发展过程
软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，即J.B提出BNF描述Algol60语言的语法，出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于 20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。经过30多年的研究和应用，如今人们在形式化方法这一领域取得了大量、重要的成果，从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。
3.3定义
用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础，那么它就是形式化的，典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的数学基础是不同的，有的以集合论和一阶谓词演算为基础（如Z和 VDM），有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。
3.4研究内容
形式化方法的一个重要研究内容是形式规约(Formal Specification,也称形式规范或形式化描述),它是对程序“做什么”(what to do)的数学描述,是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。对形式规约通常要讨论其一致性(自身无矛盾)和完备性(是否完全、无遗漏地刻画所要描述的对象)等性质。形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模,该方法通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面向性质的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系统。不同的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言(也称形式化描述语言),如代数语言OBJ、Clear、ASL、ACT One/Two等;进程代数语言CSP、CCS、π演算等；时序逻辑语言PLTL、CTL、XYZ/E、UNITY、TLA等；这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本(原子)规约,后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。
形式验证形式化方法的另一重要研究内容是形式验证(Formal Verification)。形式验证与形式规约之间具有紧密的联系，形式验证就是验证已有的程序(系统)P，是否满足其规约(φ,)的要求(即P (φ,)),它也是形式化方法所要解决的核心问题。传统的验证方法包括模拟(simulation)和测试(testing)，它们都是通过实验的方法对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行,一般的方法是在系统的某点给予输入，观察在另一点的输出,这些方法花费很大，而且由于实验所能涵盖的系统行为有限，很难找出所有潜在的错误。基于此，早期的形式验证主要研究如何使用数学方法，严格证明一个程序的正确性(即程序验证)。
3.5分类
根据说明目标软件系统的方式，形式化方法可以分为两类：
1）面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。
2）面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。
根据表达能力，形式化方法可以分为五类：
1）基于模型的方法：通过明确定义状态和操作来建立一个系统模型（使系统从一个状态转换到另一个状态）。用这种方法虽可以表示非功能性需求（诸如时间需求），但不能很好地表示并发性。如：Z语言，VDM，B方法等。
2）基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集来开发系统。如：ITL （区间时序逻辑），区段演算（DC），WP演算，时序逻辑，TAM（时序代理模型），RTTL （实时时序逻辑）等。
3）代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。与基于模型的方法相同的是，没有给出并发的显式表示。如：OBJ， Larch族代数规约语言等；
4）过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如：通信顺序过程（CSP），通信系统演算（CCS），通信过程代数（ACP），时序排序规约语言（LOTOS），计时CSP(TCSP），通信系统计时可能性演算（TPCCS）等。
5）基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系统开发和再工程带来特殊的好处。如 Petri图，计时Petri图，状态图等。
第四章UML状态图
4.1 简介
Unified Modeling Language (UML)又称统一建模语言或标准建模语言，是始于1997年一个OMG标准，它是一个支持模型化和软件系统开发的图形化语言，为软件开发的所有阶段提供模型化和可视化支持，包括由需求分析到规格，到构造和配置。面向对象的分析与设计(OOA&D，OOAD)方法的发展在80年代末至90年代中出现了一个高潮，UML 是这个高潮的产物。它不仅统一了Boo、Rumba和Jacobson的表示方法，而且对其作了进一步的发展，并最终统一为大众所接受的标准建模语言。
Grady Bo的描述对象集合和它们之间的关系的方法。James Rumb的对象建模技术（OMT）。Iva Jacobson的包括用例方法的方式。还有其他一些想法也对UML起到了作用，UML是, Jacobson。UML已经被对象管理组织（OMG）接受为标准，这个组织还制定了通用对象请求代理体系结构（CORBA），是分布式对象编程行业的领头羊。计算机辅助软件工程（CASE）产品的供应商也支持UML，并且它基本上已经被所有的软件开发产品制造商所认可，这其中包括IBM和微软(用于它的VB环境)。
4.2 历史
统一建模语言（UML）是面向对象软件的标准化建模语言。UML因其简单、统一的特点，而且能表达软件设计中的动态和静态信息，目前已成为可视化建模语言的工业标准。在软件无线电系统的开发过程中，统一建模语言可以在整个设计周期中使用，帮助设计者缩短设计时间，减少改进的成本，使软硬件分割最优。
UML的演化可以分为几个阶段[1]：第一阶段是3位面向对象（OO，Object-Oriented）方法学家Boo、Rum和Jacobson共同努力，形成了UML0.9；第二阶段是公司的联合行动，由十几家公司（DEC、HP、I-Lox、IBM、Microsoft、Oracle、TI等）组成了UML成员协会，将各自意见加入UML，以完善和促进UML的定义作，形成了UML1.0和1.1，并向对象管理组织（OMG，）申请成为建模语言规范的提案；第三阶段是在OMG控制下对版本的不断修订和改进，其中UML1.3是较为重要的修订版。
UML由3个要素构成：UML的基本构造块、支配这些构造块如何放置在一起的规则和运用于整个语言的公用机制。
UML有3种基本的构造块：事物、关系和图。
事物是对模型中最具有代表性的成分的抽象，包括结构事物，如类、协作、用例、主动类和节；行为事物，如交互、态机、分组事物、注释事物。
关系用来把事物结合在一起，包括依赖、关联、泛化和实现关系。
4.3 主要内容
UML是在Booch、OMT、OOSE等面向对象的方法及其它许多方法与资料的基础上发展起来的。UML表示法集中了不同的图形表示方法，剔除了其中容易引起的混淆、冗余或者很少使用的符号，同时添加了一些新的符号。其中的概念来自于面向对象技术领域中众多专家的思想。
UML从考虑系统的不同角度出发，定义了用例图、类图、对象图、状态图、活动图、序列图、协作图、构件图、部署图等9种图。这些图从不同的侧面对系统进行描述。系统模型将这些不同的侧面综合成一致的整体，便于系统的分析和构造。尽管UML和其它开发工具还会设计出许多派生的视图，但上述这些图和其它辅助性的文档是软件开发人员所见的最基本的构造。其中：
UML用例图与OOSE中的用例图类似。
UML的类图综合了OMT、Boo等面向对象方法中的类图。
UML状态图是对David Hare所提出状态图的改进。
UML活动图的基本语义和状态图大致相同，它类似于许多方法（包括面向对象技术之前的一些方法）中的工作流图。
UML的协作图是通过对Boo方法的对象图、Fusion方法的对象交互图以及其它一些方法中的相关图表改造而成的。
UML的构建图和部署图是在Boo方法中的模块和进程图（处理关系图、处理器图）的基础上发展起来的。
UML简化了建模方法，它扬弃了Boo、OMT或OOSE等方法中的糟粕，而代之以其它方法中的精华。UML一般不引入新的概念和符号，只有在没有现有的解决方法可以借鉴时，UML的开发者们才考虑加入新的概念。UML的开发者们是在设计一种语言（尽管只
是一种图形化语言），因此必须在简明（所有元素一律用方框和文字表示）和繁琐（为每个元素设计单独的符号）之间权衡。尽管如此，UML中还是增添了衍型和扩展机制等一些新的元素，因为这些元素在其它建模语言的实践中已经被证明是非常有用的。[2]用例图主要用来描述用户、需求、系统功能单元之间的关系。它展示了一个外部用户能够观察到的系统功能模型图。
【用途】：帮助开发团队以一种可视化的方式理解系统的功能需求。[3]
类图显示了一组类、接口、协作以及他们之间的关系。在UML中问题域最终要被逐步转化，通过类来建模，通过编程语言构建这些类从而实现系统。类加上他们之间的关系就构成了类图，类图中还可以包含接口、包等元素，也可以包括对象、链等实例。[4]对象图(Object Diagram) 是显示了一组对象和他们之间的关系。使用对象图来说明数据结构，类图中的类或组件等的实例的静态快照。对象图和类图一样反映系统的静态过程，但它是从实际的或原型化的情景来表达的。
对象图显示某时刻对象和对象之间的关系。一个对象图可看成一个类图的特殊用例，实例和类可在其中显示。对象也和合作图相联系，合作图显示处于语境中的对象原型（类元角色）。
对象图是类图的实例，几乎使用与类图完全相同的标识。他们的不同点在于对象图显示类的多个对象实例，而不是实际的类。一个对象图是类图的一个实例。由于对象存在生命周期，因此对象图只能在系统某一时间段存在。
4.4 分类
UML定义了5类，10种模型图
五种类图定义：
1.用例图：从用户角度描述系统功能，并指各功能的操作者。
2.静态图：包括类图，包图，对象图。
类图：描述系统中类的静态结构
包图：是包和类组成的，表示包与包之间的关系，包图描述系统的分层结构
对象图：是类图的实例
3.行为图：描述系统动态模型和对象组成的交换关系。包括状态图和活动图
活动图：描述了业务实现用例的工作流程
状态图：是描述状态到状态控制流，常用于动态特性建模
4.交互图：描述对象之间的交互关系
顺序图：对象之间的动态合作关系，强调对象发送消息的顺序，同时显示对象之间的交互
合作图：描述对象之间的协助关系
5.实现图：
配置图：定义系统中软硬件的物理体系结构
十种模型图定义：
（1）UML统一了各种方法对不同类型的系统、不同开发阶段以及不同内部概念的不同观点，从而有效的消除了各种建模语言之间不必要的差异。它实际上是一种通用的建模语言，可以为许多面向对象建模方法的用户广泛使用。
（2）UML建模能力比其它面向对象建模方法更强。它不仅适合于一般系统的开发，而且对并行、分布式系统的建模尤为适宜。
（3）UML是一种建模语言，而不是一个开发过程。
4.7 应用领域
UML的目标是以面向对象图的方式来描述任何类型的系统，具有很宽的应用领域。其中最常用的是建立软件系统的模型，但它同样可以用于描述非软件领域的系统，如机械系统、企业机构或业务过程，以及处理复杂数据的信息系统、具有实时要求的工业系统或工业过程等。总之，UML是一个通用的标准建模语言，可以对任何具有静态结构和动态行为的系统进行建模。
此外，UML适用于系统开发过程中从需求规格描述到系统完成后测试的不同阶段。在需求分析阶段，可以用用例来捕获用户需求。通过用例建模，描述对系统感兴趣的外部角色及其对系统（用例）的功能要求。分析阶段主要关心问题域中的主要概念（如抽象、类和对象等）和机制，需要识别这些类以及它们相互间的关系，并用UML类图来描述。为实现用例，类之间需要协作，这可以用UML动态模型来描述。在分析阶段，只对问题域的对象（现实世界的概念）建模，而不考虑定义软件系统中技术细节的类（如处理用户接口、数据库、通讯和并行性等问题的类）。这些技术细节将在设计阶段引入，因此设计阶段为构造阶段提供更详细的规格说明。
编程（构造）是一个独立的阶段，其任务是用面向对象编程语言将来自设计阶段的类转换成实际的代码。在用UML建立分析和设计模型时，应尽量避免考虑把模型转换成某种特定的编程语言。因为在早期阶段，模型仅仅是理解和分析系统结构的工具，过早考虑编码问题十分不利于建立简单正确的模型。
UML模型还可作为测试阶段的依据。系统通常需要经过单元测试、集成测试、系统测试和验收测试。不同的测试小组使用不同的UML图作为测试依据：单元测试使用类图和类规格说明；集成测试使用部件图和合作图；系统测试使用用例图来验证系统的行为；验收测试由用户进行，以验证系统测试的结果是否满足在分析阶段确定的需求。
总之，标准建模语言UML适用于以面向对象技术来描述任何类型的系统，而且适用于系统开发的不同阶段，从需求规格描述直至系统完成后的测试和维护。
4.6 发展历史
1997年，OMG组织（Object Management Group对象管理组织）发布了统一建模语言（Unified Modeling Language，UML）。UML的目标之一就是为开发团队提供标准通用的设计语言来开发和构建计算机应用。UML提出了一套IT专业人员期待多年的统一的标准建模符号。通过使用UML，这些人员能够阅读和交流系统架构和设计规划--就像建筑工人多年来所使用的建筑设计图一样
2003年，UML已经获得了业界的认同
UML的是要成为一种标准的统一语言，使得IT专业人员能够进行计算机应用程序的建模。UML的主要创始人是Jim Rum、Iva Jacobson和Grady Booch，他们最初都有自己的建模方法（OMT、OOSE和Boo），彼此之间存在着竞争。最终，他们联合起来创造了一种开放的标准。UML成为"标"建模语言的原因之一在于，它与程序设计语言无关。而且，UML符号集只是一种语言而不是一种方法学。因为语言与方法学不同，它可以在不做任何更改的情况下很容易地适应任何公司的业务运作方式。
UML不是一种方法学，不需要任何正式的工作产品。而且它还提供了多种类型的模型描述图（diagram），当在某种给定的方法学中使用这些图时，它使得开发中的应用程序的更易理解。UML的内涵远不只是这些模型描述图，但是对于入门来说，这些图对这门语言及其用法背后的基本原理提供了很好的介绍。通过把标准的UML图放进工作产品中，精通UML的人员就更加容易加入项目并迅速进入角色。最常用的UML图包括：用例图、类图、序列图、状态图、活动图、组件图和部署图
UML语言开发始于1994年8月，当时Rational软件公司的Boo和Rumba着手进行统一的Boo方法和OMT方法，以便以后得到一种统一的建模语言。1995年10月，他们发布了统一方法（UM）的级版本。同年秋天，Jacobson加盟联合开发小组，并力图把OOSE方法也统一进来
经过Boo、Rumba和Jacobson的努力，UML0.9和0.91版在1996年的6月和10月出版。1996年，OMG（对象管理组）发布了向外界征集关于面向对象建模标准方法的消息。UML的3位创始人开始与来自其它公司的软件工程方法专家和开发人员一道制定了一套OMG感兴趣的方法，并设计了一种被软件开发工具提供者、软件开发方法学家和开发人员这些最终用户接受的建模语言。与此同时，其它一些相关人员也在做这项富有竞争性的工作。1997年9月1日产生了UML1.1，并提交到OMG进行讨论。
OMG于1997年11月正式接纳了UML1.1，然后成立任务组不断的修订，并产生了UML1.2、1.3和1.4版本，其中UML1.3是较为重要的修订版本。该组织正在对UML进行重大修订，其目标是推出UML2.0，做为向ISO提交的标准方案。
James Rum等人提出了面向对象的建模技术（OMT，一种软件开发方法）方法，采用了面向对象的概念，并引入各种独立于语言的表示符。这种方法用对象模型、动态模型、功能模型和用例模型，共同完成对整个系统的建模，所定义的概念和符号可用于软件开发的分析、设计和实现的全过程，软件开发人员不必在开发过程的不同阶段进行概念和符号的转换。OMT-2特别适用于分析和描述以数据为中心的信息系统。
Jacobson于1994年提出了OOSE方法，其最大特点是面向用例(Use-Case)，并在用例的描述中引入了外部角色的概念。用例的概念是精确描述需求的重要武器，但用例贯穿于整个开发过程，包括对系统的测试和验证。OOSE比较适合支持商业工程和需求分析。
此外，还有C/Yourdon方法，即著名的OOA/OOD，它是最早的面向对象的分析和设计方法之一。该方法简单、易学，适合于面向对象技术的初学者使用，但由于该方法在处理能力方面的局限，截至2013年已很少使用。
概括起来：首先，面对众多的建模语言，用户由于没有能力区别不同语言之间的差别，因此很难找到一种比较适合其应用特点的语言；其次，众多的建模语言实际上各有
千秋；第三，虽然不同的建模语言大多雷同，但仍存在某些细微的差别，极大地妨碍了用户之间的交流。因此在客观上，极有必要在精心比较不同的建模语言优缺点及总结面向对象技术应用实践的基础上，组织联合设计小组，根据应用需求，取其精华，去其糟粕。经h和Jacobson三人的共同努力，于1996年6月和10月分别发布了两个新的版本，即UML 0.9和UML 0.91，并将UM重新命名为UML（Unified Modeling Language）。
UML是一种定义良好、易于表达、功能强大且普遍适用的建模语言。它融入了软件工程领域的新思想、新方法和新技术。它的作用域不限于支持面向对象的分析与设计，还支持从需求分析开始的软件开发的全过程。
面向对象技术和UML的发展过程可用上图来表示，标准建模语言的出现是其重要成果。在美国，截止1996年10月，UML获得了工业界、科技界和应用界的广泛支持，已有700多个公司表示支持采用UML作为建模语言。1996年底，UML已稳占面向对象技术市场的85%，成为可视化建模语言事实上的工业标准。1997年11月17日，OMG采纳UML 1.1作为基于面向对象技术的标准建模语言。
图
图聚集了相关的事物及其关系的组合，是软件系统在不同角度的投影。图由代表事物的顶点和代表关系的连通图表示。下面对常用的几类图[2-12]进行简单介绍。
（1）类图。展现了一组对象、接口、协作和它们之间的关系。类图描述的是一种静态关系，在系统的整个生命周期都是有效的，是面向对象系统的建模中最常见的图（2）对象图。展现了一组对象以及它们之间的关系。对象图是类图的实例，几乎使用与类图完全相同的标示。
（3）用例图。展现了一组用例、参与者（actor）以及它们之间的关系。用例图从用户角度描述系统的静态使用情况，用于建立需求模型。
（4）交互图。用于描述对象间的交互关系，由一组对象和它们之间的关系组成，包含它们之间可能传递的消息。交互图又分为序列图和协作图，其中序列图描述了以时间顺序组织的对象之间的交互活动；协作图强调收发消息的对象的结构组织。
（5）状态图。由状态、转换、事件和活动组成，描述类的对象所有可能的状态以及事件发生时的转移条件。通常状态图是对类图的补充，仅需为那些有多个状态的、行为随外界环境而改变的类画状态图。
（6）活动图。一种特殊的状态图，展现了系统内一个活动到另一个活动的流程。活动图有利于识别并行活动。
（7）组件图。展现了一组组件的物理结构和组件之间的依赖关系。部件图有助于分析和理解组件之间的相互影响程度。
（8）部署图。展现了运行处理节点以及其中的组件的配置。部署图给出了系统的体系结构和静态实施视图。它与组件图相关，通常一个节点包含一个或多个构建。
需要指出的是，UML并不限定仅使用这9种图，开发工具可以采用UML来提供其他种类的图，但到目前为止，这9种图在实际应用中最常用的。
4.7 应用
目前，UML已成功应用于电信、金融、政府、电子、国防、航天航空、制造与工业自动化、医疗、交通、电子商务等领域中。在这些领域中，UML的建模包括大型、复杂、实时、分布式、集中式数据或者计算，以及嵌入式系统等，而且还用于软件再生工程、质量管理、过程管理、配置管理的各方面。在软件无线电技术中，UML的应用是可行的，而且具有优势。
建模语言可被不同种类的无线电通信和H/S（Hardware/Software）描述语言所应用。软件无线电的对象需要具有可配置性及组件可重用性。系统设计阶段对语言的要求表现在功能和结构两个方面。与UML相比，一些建模语言有其自身的缺陷。比如SDL在传统意义上缺乏模块性，VHDL对软件建模来说效率不高等。
进行联合设计的UML在序列图、状态图、合作图以及实时扩展的帮助下，能很好地为组件和模块之间的相互联系构造模型，而且能在整个设计周期中使用，以帮助设计者缩短设计时间、降低改进成本并使软/硬件分割最优。功能设计需要一种对通信规范进行建模的语言，而结构设计要求一种对软件和硬件组件进行建模的语言。软件无线电可以选择许多语言，一般来讲，UML的性能在面向对象和适应性方面是较好的。UML将硬件和软件作为一个整体来进行建模。例如，由于规范的不稳定性，设计者可以从硬件移动一些协议到软件。在UML的帮助下，硬件组件和软件组件之间将会有更大的透明度。便携性和综合效率将会增加。
通常来讲，对于使用UML进行硬件软件联合设计而言可以应用下面的技术[46]：（1）UML的模型特性可帮助设计者将协议分割成硬件模块和软件模块，它们之间的相互关系可以用UML的类图或组件图进行描述；
（2）UML状态图或序列图可使交互处理的通信更加简明扼要；
（3）软件综合和硬件综合可通过使用实时嵌入式UML而被建模，实时嵌入式UML 以将并行任务分配给一个特定的处理器为目标，并将计算步骤分解到各个时钟周期中；
（4）一旦设计者通过使用类图或组件图获得接口和组件的信息，则不同种类规范的并发执行和联合仿真都将变得更容易。
综合来看，UML作为一种最合适的建模语言，其应用于软件无线电之中是可实现的，也是非常有前途的。UML在软件无线电中得以应用，必将极大地促进软件无线电技术的发展。
第五章总结与展望
总结
嵌入式系统是复杂的反应式系统，一旦系统发生故障就可能导致无法估量的严重后果。因此，采用形式化方法来保证其正确性、提高其可靠性已经成为软件工程领域一个重要研究方向。本文是从实用的角度出发，来研究嵌入式软件的功能，使用形式化方法对嵌入式软件的研究，可是软件更具有稳定性、严谨性，从而大大减少了软件故障带来的各种损失，为我们提供更加高效的产品。在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其它工程学科一样，使用适当的数学分析以提高设计
的可靠性和安全性。
展望
通过对嵌入式软件的学习和研究，我们对这个方面的知识更加了解了，对未来工作进行展望：
（1）可以从事嵌入式软件的开发
（2）可以可以从事形式化方法的研究工作
（3）大大降低嵌入式软件开发的成本
（4）得到更加稳定性、安全性的软件成品
参考文件
[1] 王晓光，冯耀东，梅宏。ABC/ADL：一种基于XML的软件体系体系结构描述语言计算机科学研究与发展。页码：41（9）：1521-1531 2004
[2] 文欣秀基于DLL实现界面组件的通用方法吉林大学出版社 2003
[3]韩晓英、虞慧群。一种用例驱动的需求关注点分离的方法[J]。电子学报。34（12A）：2498-2501 2006
[4] 三星S3C2410数据手册廖日坤. ARM嵌入式应用开发技术白金手册[M] 中国电力出版社，2005.
[5] 郑灵翔.嵌入式Linux系统设计[M] 北京航空航天大学出版社, 2008.
[6] 孙琼. 嵌入式Linux应用程序开发详解M]. 人民邮电出版社, 2006.
[7] 薛圆圆.USB应用开发技术大全[M]. 人民邮电出版社,2007.
[8] 华清远嵌入式Linux C语言应用程序设计. 人民邮电出版社，2007.
[9] Brian W.c and Dennis M. The C Programming Language(2nd Edition）[M].美国：Prentice Hall，1988.
[10] W. Richard Stevens, Stephen A. Ro. Advanced Programming in the UNIX Environment 2nd Edition[M]. 美国：Addison Wesley，2005.
致谢
首先，真诚的感谢导师马艳芳教授的悉心指导和耐心讲解以及热心鼓励，才能让我顺利的完成本次毕业论文。马老师在学术上具有敏锐的洞察力、富有创造性的思维方式以及严谨的治学，多年来一直对我影响很大，对于这次论文的圆满的完成我由衷的说一声谢谢您我的老师。