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