基于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元素、测试实例、描述、职责等。给出评审管理计划、时问表、风险、命名，编码标准、方法设计(过程，掏造型，特征，约束)。这部分是可选的，也可以通过相关的替代方式来描述。