针对如何快速开发高质量的嵌入式软件的问题，实现了一种基于MDA的嵌入式软件开发平台EUP。

该平台根据模型驱动的软件开发方法，集成UML建模、模型验证、模拟和自动代码生成技术等，为嵌入式软件的开发提供了一个统一的开发环境。分析了铁道交叉路口系统的实例，试验结果表明EUP平台能够方便、高效地实现模型模拟和验证，为快速开发高质量的嵌入式软件提供了一种可行的途径。

1． 引言

目前嵌入式系统已经广泛渗透到国民经济各个领域,如制造业、过程控制、通讯、仪器、仪表、汽车、船舶、航空、航天、军事装备、消费类产品等。为了满足嵌入式系统日益增长的复杂性[5]，需要采用模型驱动的软件开发方法并集成代码自动生成和形式化验证技术以提高嵌入式系统的开发效率和质量。但是，目前的嵌入式软件开发缺少一个统一的开发和验证环境，集成的开发平台的研究仍然不够成熟[1]。

针对该问题，将软构件重用、自动代码生成和模型验证、模拟技术集成到一个统一的开发环境中，提出一种集成的嵌入式软件开发平台。模型驱动的软件开发方法（Model Driven Development MDD）是在软件开发过程中的各个阶段生成不同的模型，并以这些模型为基础来指导整个软件开发，该方法已经引起了业界的广泛关注。模型驱动框架 (Model Driven Architecture MDA)是由OMG（Object Management Group）提出的一种基于UML、XMI、MOF、CWM等其他工业标准的框架，其核心是抽象出两个抽象级别的模型：用于表达业务逻辑的平台无关的模型 PIM(Platform Independent Models)和平台相关的模型PSM(Platform Specific Models)如J2EE等[2]。基于MDA开发嵌入式软件是实现模型驱动的嵌入式软件开发的重要途径。我们开发了基于MDA的嵌入式软件开发平台－EUP(Embedded UML Platform)，用于实现在需求分析阶段生成系统的需求分析模型，并利用形式化验证、模拟技术对模型进行验证和模拟，以确保自动生成的代码的正确性，从而满足嵌入式软件开发的高可靠性要求。

本文的组织结构如下，在简单介绍了EUP的系统结构及其功能模块划分后，重点介绍EUP的模型验证器和模拟器的功能及其关键的实现技术，并通过铁道交叉路口系统的例子说明EUP的实用性。最后，对相关的研究工作进行简单地比较，总结本文的创新之处。

2． EUP的系统结构

基于MDA开发嵌入式软件，需要在嵌入式软件开发的不同阶段构建不同的系统模型，并将这些模型作为嵌入式软件开发的基础。根据嵌入式软件开发的需要，将EUP的系统结构划分为五大功能模块：模型编辑器、模型检查器、模型验证器、模型转换器、模型模拟器，分别实现UML模型编辑、模型的语法一致性、正确性检查、利用形式化验证技术验证模型是否满足系统需要满足的属性约束、模型到代码的自动生成和模型级的功能预演。EUP的系统结构如图1所示：

图1：模型驱动的嵌入式软件开发平台的系统结构

嵌入式软构件库

PSM（目标系统）

模型检查器

模型编辑器

模型模拟器

模型验证器

语言编译器

PIM（UML）模型

模型转换器

操作系统适配器

嵌入式系统开发的初期，可以在“模型编辑器”中构建与平台无关的模型PIM，如UML用例图、类图、状态图、对象图、顺序图、活动图、协作图等描述系统，用以帮助澄清用户需求；绘制好的UML模型可以用“模型检查器”检查其语法的正确性，以确保在编辑器中生成的模型遵循UML2.0的元模型；“模型验证器”采用形式化的模型验证技术对语法正确的UML模型进行形式化的模型验证，从而验证系统模型是否满足系统的属性约束等。由于状态图是一种“面向对象的可操作状态图”，可以被用来构建嵌入式系统的原型，并可通过“模型模拟器”模拟执行嵌入式系统的原型；把通过验证的UML模型送入“模型转换器”(Model Complier)中进行编译,可以自动生成基于抽象操作系统接口的代码（C、C++等）。基于后台的嵌入式软构件库，EUP可以基于软构件的软件开发方法，重用已有的嵌入式软构件，提高软件的开发效率。将EUP自动生成的代码和嵌入式软构件进行链接、组装后得到的代码经过操作系统适配器和对应的语言编译器的处理，就可生成依赖于特定嵌入式操作系统的目标系统（PSM），即可被传输到具体的嵌入式硬件中进行最终的测试和使用。

3． 各个功能模块的介绍

基于EUP的体系框架其各个功能模块之间密切合作，在嵌入式软件开发的不同阶段实现不同的功能，为构建一个集成的嵌入式软件开发环境提供了条件。下面重点介绍EUP中的几个功能模块：

3.1模型编辑器

模型编辑器能够提供可视化的模型编辑界面，用以构建UML类图、对象图、状态图、顺序图、活动图、协作图，实现对嵌入式系统的静态特性和动态特性进行建模。这些模型严格遵循UML2.0元模型的规范标准，并以XML文件的格式被保存下来。

3.2 模型验证器

EUP中的模型验证模块分成两个部分：功能属性的验证（UML verification environment UVE）和非功能属性的验证（timed UML verification environment TUVE）。功能属性的验证主要指验证模型是否满足和系统的功能相关的属性如安全性或者活性等，以满足嵌入式系统的高可靠性要求。安全性指无效终止状态和断言冲突，活性指验证系统是否存在环路。此外，实时嵌入式系统还必须满足和时间相关的非功能属性，因此，时间属性的验证是保证实时嵌入式软件满足时间约束的重要途径。这里，非功能属性的验证特指时间属性的验证。EUP的集成验证环境如图2所示，其中在UVE中使用UML类图来描述系统的结构特性，状态图来描述系统的动态特性，使用预先定义的时态逻辑模式来定义系统的时间约束等，并在出现错误时给出的错误的反例以方便建模者定位错误。TUVE使用时间状态图建模系统并可使用对OCL（Object Constraint Language）进行实时扩展后得到的RT-OCL描述时间约束，其反例的显示和UVE一样，可以有两种显示方式：文本或者扩展的顺序图（ESD）。从图2可以看出EUP的模型验证器将验证工具SPIN[3]作为其后台的支撑工具，以完成模型验证功能。

图2：EUP的验证环境

3.2 模型模拟器

模型模拟器的功能是模拟执行嵌入式系统的原型，实现模型级的功能预演。通过验证的嵌入式系统的模型，可以在模拟器中进行模拟执行。模型模拟是实现大规模、高质量的嵌入式软件开发的关键技术。在EUP中，模型模拟器根据UML状态图的操作语义[4]，实现状态图的动态模拟算法。该算法支持UML状态图中的并发状态、层次状态、或状态等的模拟执行，解决了UML状态图的动态执行问题。

在模型模拟器中，系统的当前活动状态收到触发事件后，当满足触发条件时就执行一步，系统进入下一个状态。同时，为了更好的记录系统状态变化的整个过程，使用消息顺序图记录系统状态的变化过程和导致这些变化的触发事件。

4． 铁道交叉路口的示例

下面通过经典的铁道交叉路口系统（Railroad Crossing System, 简称RCS）的例子来说明EUP的实用性。RCS是一个典型的嵌入式系统，它使用软件控制一个通常的铁道口的控制门。由A处的探测器检测火车的临近：当火车经过探测器时，该探测器发送通知nearby；火车经过探测器A后，至少经过300个单位时间到达门的位置。火车到达B时，发送通知open，然后路口处的门打开，且门从完全关闭到完全打开的时间为100个单位时间；从完全打开到完全关闭的时间是20个单位时间；探测器E检测火车是否通过该路口，若通过则发送消息entered。After(100)后，火车才完全通过铁道口的控制门，图3(b)描述了RCS系统的时间表示。

首先，在模型编辑器中生成RCS的类图如图4所示，该例子涉及到三个类：门、铁道和控制器，并且根据实际应用中可能出现的状态为每个类创建其对应的状态图。

图4：RCS的类图

接下来，使用模型模拟器对通过验证的模型进行模拟执行，进一步地分析系统模型的实际执行情况。图5描述了RCS中的三个状态图的执行过程，模型模拟器的界面的上半部分是状态图的当前执行状况，其中红色状态表示系统目前的活动状态，红色箭头表示当前的状态转换；界面的下半部分是记录状态图的整个执行过程的消息顺序图，该顺序图是根据系统状态的执行过程而自动生成的。

图5：RCS例子的模拟执行情况

5． 结论

研究嵌入式软件开发平台的代表性工作主要有：由德国Paderborn大学开发的Fujaba 工具集其主要功能是实现UML类图、状态图到代码的自动转换；Lilius等开发的vUML用于将UML状态图转换为验证工具SPIN的输入语言 Promela，从而实现状态图的模型验证等；与已有的工作相比，本文作者主要创新点：EUP集成了UML建模技术、软构件技术、形式化模型验证、模拟和代码自动生成技术，实现了在同一个开发环境中进行嵌入式系统的模型编辑、验证、模拟及代码的自动生成等。此外，EUP基于MDA的框架，为高效地开发高质量的嵌入式软件提供一种可行的途径。

参考文献：

[1] Susanne Graf and Jozef Hooman, Correct Development of Embedded systems [C], EWSA04, 2004

[2] Anneke Kleppe, Jos Warmer, WimBast MDA Explained: The Model Driven Architecture: Practice and Promise, [M] Addison Wesley, April 2003

[3] G.Holzmann, The model checker SPIN[C], IEEE Transactions on Software Engineering, 1997,23(5),279-295.

[4] D. Harel and A. Naamad. The STATEMATE semantics of statecharts.[C] ACM Transactions on Software Engineeringand Methodology, Oct 1996,5(4):293–333.

[5] 马正华; 孙玉强; 史海锋; 王明斐，嵌入式多重识别智能门禁系统的设计，微计算机信息，2005 年第21 卷第12-2 期 第4-5页