件规约系统（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）面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。