基于时序逻辑的工作流建模与分析方法  

Modeling and analysis of workflows based on temporal logics

作　　者：王远[1] 范玉顺[1] 

机构地区：[1]清华大学自动化系,北京100084

出　　处：《高技术通讯》2006年第2期157-162,共6页Chinese High Technology Letters

基　　金：国家自然科学基金（60274046）资助项目

摘　　要：提出了一种基于活动时序逻辑（TLA）的工作流建模与模型分析的形式化方法。该方法将模型及模型的性质都表示为一个，TLA公式，对工作流模型性质的分析可以等价为对，TLA中两个公式之间是否存在蕴涵关系的检验，从而建立了一个工作流模型各层次分析统一框架。一个工作流建模和分析的实例验证了所提出方法的有效性，该方法在建模、模型分析以及指导模型设计等方面都有较好的应用前景。This paper presents a method for modeling and analyzing workflows based on temporal logic of actions （TLA）. After a brief review of TLA, it presents the semantics of workflow process using TLA and illustrates how to model and analyse workflows using TLA. In TLA, both the workflow model and its properties are modeled by TLA formulas. Analysis of workflow model in TLA is carried out by verification of the implication relationship between two formulas. Finally, the process of modeling and analysis is validated through a case study.

关 键 词：工作流 活动时序逻辑 工作流模型分析 

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