基于时间自动机的实时工作流时序约束一致性验

2009年 12月 JOURNAL OF SUZHOU UN I VERSITY( ENGINEER ING SCIENCE ED ITI ON) Dec . 2009 收稿日期: 2009 - 09 - 09 作者简介: 龙世荣 (1974 - ) ,男 ,硕士研究生 ,讲师 ,主要研究方向为实时系统与形式化方法。 基金项目: 中国科学院计算机科学国家重点实验室开放课题 (编号 SYSKF0908) ;江苏省高校自然科学基金项目 (编号 08KJB520010)。 文章编号: 1673 - 047X(2009) - 06 - 0012 - 05 基于时间自动机的实时工作流时序约束一致性验证 龙世荣1, 2 ,张广泉1 ,汪宏海3 (1.苏州大学计算机科学与技术学院,江苏 苏州 215006; 2.广西教育学院现代教育技术系,广西 南宁 530023; 3.赣南教育学院计算机系,江西 赣州 341000) 摘　 要: 提出一种基于时间自动机的实时工作流时间建模与验证方法。该方法首先将实时工作流 的时间工作流图转换成时间自动机模型 ,再利用时间自动机的机制验证其时序约束一致性。 关键词: 实时工作流;时间自动机;一致性验证 中图分类号: TP311　　　　 文献标识码: A 0　 引　 言 与一般的工作流系统不同 ,在实时计算机系统中 ,时效性对其正确运行极其重要。在实时工作流系统中 , 违反时序约束有可能导致严重的后果。因此 ,对实时工作流进行时间建模并对其时序约束的一致性进行验 证 ,以确保实时工作流的每个任务都满足时序约束要求 ,有着非常重要的意义。而利用传统的工作流技术则 很难实现这个要求。 本文使用时间自动机作为实时工作流时间建模及时序约束验证的工具。文章介绍了如何将实时工作流 图转化成时间自动机模型 ,并利用时间自动机的机制验证实时工作流时序约束的一致性。 1　 实时工作流及其研究现状 自 20世纪 80年代出现工作流技术以来 ,不同的研究者和研究机构对工作流分别提出了不同的定义。这 些定义都反映了这些基本问题:业务过程是什么 (一系列的活动和任务 ) ? 谁去做 (参与者 ) ? 怎么做 (活动的 执行条件 ,控制流和信息的定义 ) ? 在参考 WFMC的工作流定义的情况下 ,我们将实时工作流定义为:在实时 环境下 ,按照业务对时间性能的约束 ,能够在各个应用系统之间根据一系列规则完全自动执行的业务过程。 实时工作流中最关键的任务之一是工作流时间管理。但是 ,目前工作流管理系统提供的时间管理支持非 常有限。现有的一些时间管理方法多数基于图论方法[ 1 - 6 ] 。他们通常的做法是扩展工作流图 ,在工作流图状 态节点上嵌入活动的时间信息、 或在工作流图的边上嵌入活动间的时间约束信息 ,如 J . Eder等人在文献 [ 1 - 2 ]中使用活动持续时间和关键路径方法验证时序约束一致性 ,而文献 [ 6 ]则对 UML状态图进行时间扩 展 ,并使用时钟事件表示工作流中的时序约束。 2　 工作流图及其时间扩展