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

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

作　　者：杜彦华[1] 范玉顺[2] 

机构地区：[1]北京科技大学机械工程学院,北京100083 [2]清华大学自动化系,北京100084

出　　处：《机械工程学报》2010年第2期185-191,共7页Journal of Mechanical Engineering

基　　金：国家自然科学基金(60674080);国家高技术研究发展计划(863计划;2006AA04Z151;2006AA04Z166)资助项目

摘　　要：现实企业中通常存在多个并行的工作过程,并且它们之间可能存在资源冲突。在运行阶段,动态验证资源约束下多个过程的时序一致性具有重要意义。基于实时模型检测技术,提出一种工作流多过程时序一致性动态验证方法。采用时间自动机(Time automata,TA)对多个并发过程建模,并将所需验证的时序约束转化为对TA模型的性质查询。当运行到检测点,依据已知的时间信息更新TA模型,再进行相关性质查询,从而完成时序约束的验证。该方法实用性较强,能够有效处理现实业务环境中资源约束情况下多个业务过程的动态时序验证问题。具有较好的柔性和扩展性,当时序约束发生变化时,仅需改变相应TA模型。本方法有多种实时模型检测工具或软件的支持。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-proce,;s of workflows is modeled by using a time automata, and the temporal constraints to be checked are transformed as the queries of ,observer time ant omata 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 ant omata is changed. Furthermore, there are some tools and software of real-time model checking to support it.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]