使用扩展区间时序逻辑为并发工作流建模

Modelling concurrent workflow with the extended interval temporal logic

针对集中式体系结构并发工作流的两种运行方式(活动并发执行和活动以任意顺序执行),对区间时序逻辑进行扩展,提出两个新操作符"交错"和"限制性交错".根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系,证明用新操作符连接的区间时序逻辑公式适于表示并发工作流.结合一个并发工作流实例,说明如何用扩展区间时序逻辑表示活动及由活动组建的并发工作流,从而得到并发工作流的区间时序逻辑模型.利用并发工作流的区间时序逻辑模型验证并发工作流的活性和安全性,可大大提高并发工作流设计的可靠性.

According to the concurrent workflow patterns, split and anyorder, and their implementation in the systems adopting the central architecture, the interval temporal logic is extended by two new operators： shuffle and restricted shuffle. The formulas connected with the new operators are suitable for representing concurrent workflows, which is proved with the partlal-order relationship among the states maintained by the workflow and the length relationship among the intervals that satisfy those formulas describing the workflow and the participating activities. An example is given to illustrate how to use the extended interval temporal logic to represent the activities and the concurrent workflow composed of these activities. The interval temporal logic model for concurrent workflows can be obtained by this method. This model can be employed to verify the liveness and safety of concurrent workflows by utilizing some tools and theories based on interval temporal logic, which guarantees the reliability of the design of concurrent workflows.