摘要
提出了一种基于活动时序逻辑（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.
出处
《高技术通讯》
CAS
CSCD
北大核心
2006年第2期157-162,共6页
Chinese High Technology Letters
基金
国家自然科学基金（60274046）资助项目
