现实企业中通常存在多个并行的工作过程,并且它们之间可能存在资源冲突。在运行阶段,动态验证资源约束下多个过程的时序一致性具有重要意义。基于实时模型检测技术,提出一种工作流多过程时序一致性动态验证方法。采用时间自动机(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.