JOURNAL OF COMPUTERS (JCP)
ISSN : 1796-203X
Volume : 4    Issue : 1    Date : January 2009

Modeling and Analysis of Workflow Based on TLA
Shu Chen and Guo Qing Wu
Page(s): 27-34
Full Text:
PDF (170 KB)


Abstract
We proposed an approach in modeling and analysis of workflow based on temporal logic of action.
A workflow model is divided in to two parts: the description of scheduler as well as database
updating and the description of properties, each part is expressed in a TLA formula. The analysis of
properties is composed by scheduling analysis and database properties analysis and their proof
process is equivalence to the verification of the implementation relationship between the model
formula and the formula of its properties. Thus, established an unified framework for modeling and
property analysis of workflow in deferent levels.

Index Terms
workflow, TLA, modeling, property analysis