一种进程代数风格的基于时序逻辑的工作流建模方法

摘要

针对工作流系统，提出使用基于进程代数风格的操作时序逻辑(TLA)来对工作流的建模以及特性做整体分析的方法。其中基于TLA的工作流模型分为描述工作流过程控制、数据更新和描述工作流基本特性两部分，并分别表示为TLA公式。工作流性质的验证分为过程性质验证以及数据性质验证。特性验证过程则可以等价为分析模型TLA公式到特性TLA公式之间蕴含关系的检验，从而建立了工作流调度及其数据各层次分析的统一框架。实例分析证明了该方法的有效性。