基于UML状态图和Petri网的冷却水实时控制系统建模

( ) 第 29 卷第 6 期 苏 　州 　大 　学 　学 　报 工 　科 　版 Vol29 No. 6 2009 年 12 月 JOURNAL OF SU ZHOU UN IV ER SITY ( EN GIN EER IN G SC IENCE ED ITION ) D ec. 2009 文章编号 : 1673 - 047X (2009) - 06 - 0007 - 05 基于 UML 状态图和 Petr i网的冷却水实时控制系统建模与分析 杨喜刚 ,张广泉 (苏州大学计算机科学与技术学院 ,江苏 苏州 2 15006) 摘 　要 : 实时系统应用要求其必须有严格的正确性 , UML 及 Petri 网是保证其正确性的重要建模与 分析方法 。通过介绍 Petri网的基本模型 ,阐述了 UML 状态图到 Petri网模型的转换规则 ,通过生产 线冷却水控制系统的实例描述了其在实时控制系统中的应用 。 关键词 : 实时系统 ;形式化方法 ; UML 状态图; Petri网;冷却水控制系统 中图分类号 : TP3 11　　　　文献标识码 : A 0　引　言 实时系统在工业 、军事和商业等领域有着广泛的应用 ,如消费类电子设备 、空中交通控制 、机器人 、工业 自 动控制等 。实时系统不仅要求其执行产生的结果在逻辑上是正确的 ,而且要求其在时间上也是正确的。实时 性及并发性是实时系统的两个基本特性 。对于实时系统 ,确保其正确性及安全性是至关重要的 ,对系统进行 建模与分析是一种重要的保证手段 。当前主流的实时系统建模方法主要有统一建模语言 UML 和形式化方法 两类 。 UML 源自 OM G于 1997年采纳的第一个开放的 OO 可视化建模语言 ,它结合了 Booch 方法 、OM T方法和 OO SE方法 ,统一了面向对象方法的基本概念 。UML 虽具有可视化的特点 ,但其缺乏精确的语义 。如在多系 统级任务并发执行的环境下 , UML 不能描述各个对象之间的交互 ,也不能确定执行是否处于并发状态 [ 1 ] 。形 式化方法建立在严格的数学基础之上 ,能够对对象 、动作等进行简洁 、准确的描述 。 基于两种建模方法各自的优缺点 ,不少研究者提出了将两者相结合的方法 ,通过 UML 扩展机制 ,将 UML 模型转换为相应的形式化模型 ,然后通过形式化方法对模型进行分析 。文献 [ 2 ]采用可执行的线性时序逻辑 语言 XYZ / E对 UML2. 0 的顺序图和状态图进行了形式化定义 ,为使用 UML 和形式化方法相结合描述软件体 系结构的交互行为奠定了基础 。文献 [ 3 ]给出了将 UML 顺序图以及类图转换为 Petri网模型的方法 ,进而采 用 Petri网分析方法对 UML 模型进行分析与验证 ,避免了直接进行 Petri网建模过程的繁琐 ,弥补了 UML 缺少 模型分析 、验证手段不足的缺点 。文献 [ 4 ]使用了一定的转化规则 ,将 UML 状态图模型转化成 Petri网模型 , 使用 Petri网的可达树对系统进行分析 。 生产线冷却水控制系统是一个典型的实时控制系统 ,运行过程中 ,根据系统中各检测设备的状态 ,相应改 变系统中运行设备的运行状态 ,使冷却水控制在一个合理的范围之内。验证其能否满足设计需要 ,是开发该 控制系统的一个关键环节 ,因此需要对该控制系统进行建模分析 。本文采用 UML 状态图与 Petri 网相结合 , 首先对系统的状态进行 UML 建模 ,然后根据一定的转化规则 ,将 UML 状态图转化到 Petri网 ,通过 Petri网的 可达树进行分析 ,判断系统的实时特性是否符合要求 。 收稿 日期 : 2009 - 08 - 06 ( ) 作者简介 : 杨喜刚 1972 - ,男 ,硕士研究生 ,主要研究方向为实时系统与形式化方法 。 ( )