文献类型：期刊文章

作　　者：雷丽晖[1] 段振华[1]

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071

出　　处：《西安电子科技大学学报》

基　　金：国家自然科学基金资助(60373103);国家自然科学基金重点项目资助(60433010)

年　　份：2007

卷　　号：34

期　　号：4

起止页码：673-680

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CAS、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20073710810522)、IC、INSPEC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

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

关 键 词：并发工作流  区间时序逻辑 确定有限自动机

分 类 号：TP393]