• CN:11-2187/TH
  • ISSN:0577-6686

›› 2010, Vol. 46 ›› Issue (2): 185-191.

• 论文 • 上一篇    下一篇

工作流多过程动态时序一致性的实时模型检测

杜彦华;范玉顺   

  1. 北京科技大学机械工程学院;清华大学自动化系
  • 发布日期:2010-01-20

Real-time Model Checking of Dynamic Temporal Consistency for Multi-process of Workflow

DU Yanhua;FAN Yushun   

  1. School of Mechanical Engineering , University of Science and Technology Beijing Department of Automation, Tsinghua University
  • Published:2010-01-20

摘要: 现实企业中通常存在多个并行的工作过程,并且它们之间可能存在资源冲突。在运行阶段,动态验证资源约束下多个过程的时序一致性具有重要意义。基于实时模型检测技术,提出一种工作流多过程时序一致性动态验证方法。采用时间自动机(Time automata,TA)对多个并发过程建模,并将所需验证的时序约束转化为对TA模型的性质查询。当运行到检测点,依据已知的时间信息更新TA模型,再进行相关性质查询,从而完成时序约束的验证。该方法实用性较强,能够有效处理现实业务环境中资源约束情况下多个业务过程的动态时序验证问题。具有较好的柔性和扩展性,当时序约束发生变化时,仅需改变相应TA模型。本方法有多种实时模型检测工具或软件的支持。

关键词: 动态验证, 多过程, 时间自动机, 时序约束, 实时模型检测

Abstract: In the practical operation environment of an enterprise, there generally exist multiple parallel working processes, thus having resource conflicts among them. It is very important to model and verify dynamically the consistency of temporal constraints of multi-process with resource conflicts. Based on real time model checking technique,a dynamic checking method of temporal constraints for multi-process of workflows is proposed. Multi-process of workflows is modeled by using a time automata, and the temporal constraints to be checked are transformed as the queries of observer time automata models. When temporal constraints are checked, the models are updated according to the known temporal information, and temporal constraints are checked. The method is practicable, because it not only can deal with the modeling and analyzing of multi-process with resource constraints, but also is flexible, namely when the temporal constraints are modified, the corresponding observer time automata is changed. Furthermore, there are some tools and software of real-time model checking to support it.

Key words: Dynamic checking, Multi-process, Real-time model checking, Temporal constraint, Time automata

中图分类号: