基于UML与Petri网的嵌入式系统设计与验证-UML软件工程组织-火龙果软件

UML软件工程组织

基于UML与Petri网的嵌入式系统设计与验证

来源：电子技术应用作者：茂名学院自动化系廖晓文刘美

摘要：提出了一种基于UML与Petri网的嵌入式系统设计与验证的方法，详细讨论了该方法的主要应用流程，并给出了一个应用实例。

关键词：嵌入式系统设计UML语言Petri网验证

在嵌入式系统设计中采用模型的方法，有利于保证系统的正确性，缩短开发周期，降低开发费用。作为面向对象的建模技术，统一建模语言UML可以将复杂的系统设计简单化，并能从需求分析、设计到实现等各阶段为嵌入式系统开发人员提供有力支持。但UML缺乏精确的语义描述，因此无法对用UML建立的嵌入式系统模型进行形式化的分析和验证。Petri网建模方法基于严格的数学理论，使用形式化规范对系统建模，并且可以通过众多的工具完成验证。但Petri网建模方法不直观．在需求获取、交流等方面存在无法克服的弱点。

UML与Petri网相结合的建模方法能实现二者互补，既能有效获取需求、分析设计，又能进行严格建模、形式化验证。UML与Petri网结合建模的主要研究和应用都集中于工作流的建模。本文在上述背景下研究了基于UML和Petri网的嵌入式系统设计与验证的方法。

1 相关研究

目前，已经有几种影响比较大的、基于UML的、用于嵌入式系统设计的语言和建模方法，如RTUML、COMET、ROPES。

在嵌入式系统的UML模型检验方面，也出现了一些利用UML的状态图对模型进行检验的方法。这些方法都是把UML的状态围翻译为现有模型检验工具的输入语言(如SPIN、SMV)后加以验证，但对模型而言，它们不是最自然、最有效的方法。首先它忽视了系统的静态结构特征；其次，翻译后会引入较多的冗余，而且由于意义不同需要额外处理。并且这种只能检验部分性质的方法涉及到许多形式化内容，一般软件开发人员难以掌握。因此，这种方法的使用范围相当有限。

随着嵌入式系统的广泛应用，产生了多种扩充的Petrl网模型。其中，最典型的有OPNets(0bject OrientedHigh-Level Petri Nets)、ETPN(Emended Time Petri Nets)和PRES(Petri net based Representation for Embedded Systems)由于自身的原因，Petri网在捕获用户的需求、实现细节与需求分开、交流等方面有难以克服的弱点。同时，Petri网只是一种用来描述和分析系统模型的工具，不是计算机的实现工具，必须采用一定的方法通过软件才能实现。

2 方法架构

本文针对嵌入式系统实时、并发、事件驱动等特性，借鉴COMET、ROPES、OPNets、ETPN和PRES等影响比较大的、基于UML或者Petri网的嵌入式系统设计建模方法，提出UML与Petri网的嵌入式系统设计与验证方案。其方法构架如图l所示。

具体说明如下：

(1)创建系统协作图(环境图，Context Diagram)以说明对象，数据的输入输出。创建需求可追踪性表，列出需求名、需求号、引用、用例、UML元素、测试实例、描述、职责等。给出评审管理计划、时问表、风险、命名，编码标准、方法设计(过程，掏造型，特征，约束)。这部分是可选的，也可以通过相关的替代方式来描述。

(2)充分利用用例描述系统需求。嵌入式系统需要与外部环境交互。重要的外部对象及其对系统的交互构成系统需求分析的基础。在需求描述阶段不考虑设计因素，只定义系统各方面的行为。这个阶段相当于一般的嵌入式系统设计中的产品定义阶段。

(3)分析需求，确定硬件和软件之间的分界(即软硬件划分)，创建一个高级的系统体系结构，将复杂控制算法精化和特征化。划分完后进人硬件设计阶段，可按上所述设计过程开发硬件。相对简单的系统可以跳过这一步骤。

(4)利用UML的静态图描述系统的静态模型。定义系统中对象的类、类的属性、类之间的关系及每个类的操作。

(5)对象分析，确定参与每一个用例的对象及相互间关系。对象可以是实体对象、接口对象(设备接口、用户接口、系统接口)、控制对象和应用逻辑对象。

(6)利用UML的动态图描述系统的动态模型。开发对象的交互图，显示参与用例的对象之间交互的次序，分析对象问交互的次序及传送的信息。同时，为每个状态依赖协作图中的对象开发一个状态图，识别这些关键抽象如何响应外部和内部激励，以及它们如何动态协作以获得系统级的功能。

(7)进入设计建模阶段，综合分析模型，采用迭代的方式得到整个软件的体系结构。

(8)将类图和状态图转换为相应Petri网模型并分析验证。如模型不正确，则需重新审视其设计。如果正确，则进行构件映射，以节约此后相关开发的时间。对于构件，应按照可重用的要求进行设计、实现、打包和编写文档。

由于嵌入式系统通常为实时系统，而且许多嵌入式系统特别强调程序的实时特性，因此，设计一个嵌入式系统时需要考虑此系统是否有时问的限制。这些时间限制可能是局部的或者是全局的，区别在于这个时间限制相对于整个系统的位置。在编写程序时，必须满足这些限制，避免实际执行时超出时间限制所造成的影响。在这方面，可以将序列图转换为时间Petri网来进行程序排程验证。此外，对于内部交互比较复杂的子系统，为达到良好的建模效果，可直接运用OPNets进行设计，使子系统开发实现形式化与可视化，同时使建模、模拟与运行一体化。

3 应用实例

本文所举应用示例为：商家拥有三台客户税控机，一台服务器税控机，服务器税控机直接控制两台发票打印机，为有需要的顾客打印发票。即顾客向客户机操作员提出申请，操作员向服务器税控机申请执行相关操作，服务器税控机将要打印的发票信息输送到两台打印机中的一台，顾客到发票打印机处取发票。为节约成本，客户端采用8位单片机，服务器采用32位单片机。

按照前面所述方法，建立了系统相关的类图和状态图，如图2、图3、图4、图5所示。

在描述状态图和类图方面，本文遵循的原则为：事件(events)和动作(actions)必须表示为有效的方法(methods)。一个状态图中的类能够监听请求其方法(request(<method>))的事件，也能够发出所请求的方法已完成(commit(<method>))的信号。对于状态图中的动作，既可以是请求一个外部服务(request(<method>))，也可以是执行一个方法(ser(<method>))。

通过将UML图映射到Petri网，便可以对UML定义采取严格正式的分析了。Petri网支持多种不同开销和精度的分析方法，如模拟、可达树、关联矩阵、状态方程。这里主要讨论动态方面的主要技术：模拟、可达树。

模拟包括建立一个使燃顺序并将其表示为UML状态。模拟要耗费相当的计算资源并且是自动化的。它能够揭示缺陷，并为最终用户提供重要的信息反馈，因此它支持对定义的验证。例如，通过图6所示的Petri网进行模拟可以使用户理解系统的最终行为，因此能够在早期验证定义发现可能存在的问题。通过分析图6的模拟执行序列，可以发现这个模型明显不正确，因为它可以允许顾客打印与他们所购买商品不同的发票清单。在本例中。问题可以追溯到设计时的错误：软件工程师没有指定顾客应该到哪一个打印机取发票，因此Customer1可以到PrInter2打印发票，而实际上Printer2是为Customer2开的。通过模拟可以发现问题，但不能保证不会出现与预期不相符的行为。

可达树用以描述Petri网的可达(标识)集，它既与Petri网的结构有关，也与Petri网的初始标识有关。通过分析Petfi网的可达树，可了解Petri网的许多重要性质，如有界性、安全性、守恒性、可达性、覆盖性甚至死锁和活性等。对从UML模型转换过来的Petri网模型，可达树法还可以保证类定义性，被证明是一种有效的分析方法。但它穷举所有有限的可能状态进行计算，因此只适合验证比较小的Petri网系统。对于一般的嵌入式系统而言，利用模拟分析的方法已足够。

同时，对于内部交互比较复杂的子系统，可以直接运用OPNets进行设计和验证。

本文提出的方法充分发挥了UML和Petri网的长处，能够支持从需求分析到模型实现的全生命周期。用这种方法为嵌入式系统建模具有以下优点：(1)具有模块化功能和可重用性；(2)实现了对用户友好的可视化设计；(3)UML模型与计算机程序设计语言联系紧密，易于模型实现。

由于本文所举的示例较为简单，所以可以用手工为其建模、分析。对于比较复杂的系统有时需要借助一些计算机辅助工具来建模和分析。目前，关于Petri网的计算机辅助工具和基于UML的可视化建模工具已经相当成熟，但从UML模型到，Petri网的转换工具还未出现，作者正在从事这方面的研究工作。可以相信，随着这一问题的解决，集成UML与Petri网方法在未来嵌入式系统建模领域会发挥越来越重要的作用。