| 摘要 | 第4-5页 |
| ABSTRACT | 第5页 |
| 注释表 | 第11-12页 |
| 第一章 绪论 | 第12-19页 |
| 1.1 研究背景 | 第12页 |
| 1.2 研究现状 | 第12-16页 |
| 1.2.1 时间模式研究现状 | 第12-13页 |
| 1.2.2 业务流程模型研究现状 | 第13-15页 |
| 1.2.3 业务流模型一致性验证研究现状 | 第15-16页 |
| 1.3 研究目的与意义 | 第16页 |
| 1.4 主要研究内容 | 第16-19页 |
| 第二章 基于形式化语义的时间模式分析 | 第19-47页 |
| 2.1 时间模式的定义与分类 | 第19-26页 |
| 2.1.1 基于设计选择参数的时间模式定义 | 第19-25页 |
| 2.1.2 基于时间资源规划的时间模式分类 | 第25-26页 |
| 2.2 业务流图与时间区间的形式化定义 | 第26-33页 |
| 2.2.1 业务流图的语法语义介绍 | 第26-27页 |
| 2.2.2 时间区间属性的描述 | 第27-28页 |
| 2.2.3 时间区间关系的性质 | 第28-31页 |
| 2.2.4 业务流图的形式化描述 | 第31-33页 |
| 2.3 时间模式的形式化描述 | 第33-41页 |
| 2.3.1 持续时间模式的形式化描述 | 第33-35页 |
| 2.3.2 固定时刻模式的形式化描述 | 第35-36页 |
| 2.3.3 同回路周期循环模式的形式化描述 | 第36-37页 |
| 2.3.4 不同回路周期循环模式的形式化描述 | 第37-41页 |
| 2.4 时间模式之间的转换及其可满足性保持定理 | 第41-46页 |
| 2.4.1 周期循环模式与持续时间模式的转换规则 | 第41-43页 |
| 2.4.2 时间模式的可满足性定义 | 第43-44页 |
| 2.4.3 时间模式的可满足性保持定理 | 第44-46页 |
| 2.5 本章小结 | 第46-47页 |
| 第三章 基于时间模式形式化分析的业务流程模型验证 | 第47-71页 |
| 3.1 业务流程模型概述与验证框架 | 第47-49页 |
| 3.2 业务流程模型到Prolog的转换 | 第49-62页 |
| 3.2.1 静态结构的转换规则与转换算法 | 第49-53页 |
| 3.2.2 动态行为的转换规则与转换算法 | 第53-56页 |
| 3.2.3 业务流图的转换规则与转换算法 | 第56-62页 |
| 3.3 业务流程模型一致性到Prolog的转换与验证 | 第62-70页 |
| 3.3.1 静态结构一致性的转换与验证 | 第62-64页 |
| 3.3.2 动态行为一致性的转换与验证 | 第64-66页 |
| 3.3.3 时间模式一致性的转换与验证 | 第66-70页 |
| 3.4 本章小结 | 第70-71页 |
| 第四章 基于时间模式分析的业务流程模型验证平台实现与应用 | 第71-84页 |
| 4.1 基于时间模式的业务流程模型验证平台设计 | 第71-76页 |
| 4.1.1 开发环境以及设计架构 | 第71页 |
| 4.1.2 平台业务需求 | 第71-73页 |
| 4.1.3 平台模块设计 | 第73-76页 |
| 4.2 基于时间模式的业务流程模型平台应用 | 第76-83页 |
| 4.2.1 业务流程平台建模 | 第76-81页 |
| 4.2.2 验证与结果分析 | 第81-83页 |
| 4.3 本章小结 | 第83-84页 |
| 第五章 总结与展望 | 第84-85页 |
| 5.1 主要工作 | 第84页 |
| 5.2 后续工作展望 | 第84-85页 |
| 参考文献 | 第85-89页 |
| 致谢 | 第89-90页 |
| 在学期间的研究成果及发表的论文 | 第90页 |