第一章 绪论 1
1.1 电子商务 1
1.1.1 电子商务定义 1
1.1.2 电子商务系统体系 2
1.2 电子商务系统的特点 4
1.3 工作流管理系统（WfMS） 5
1.3.1 基本概念 5
1.3.2 体系结构 6
1.3.3 电子商务中的工作流 8
1.4 电子商务系统形式化技术综述 9
1.4.1 一般形式化方法 9
1.4.2 基于逻辑的方法 10
1.4.3 基于Petri网的方法 11
1.4.4 基于工作流网的方法 13
1.4.5 四类形式化方法比较及本文工作的重要性 13
1.5 约定和假设 16
1.6 本文的研究动机和贡献 16
1.6.1 研究动机 16
1.6.2 主要研究内容 18
1.6.3 主要贡献 19
1.7 内容的组织 19
第二章 基本知识 21
2.1 Petri网（PN） 21
2.1.1 Petri网概念 21
2.1.2 Petri网性质 23
2.1.3 谓词／变迁（Pr/T）网 23
2.1.4 有色Petri网（CPN） 25
2.1.5 时间Petri网（TPN） 26
2.2 时序逻辑 27
2.2.1 基本概念 27
2.2.2 时序逻辑系统 28
2.3 工作流网 29
2.3.1 形式定义 29
2.3.2 工作流网性质 30
第三章 电子商务系统时序性质分析与验证 32
3.1 时序性质 32
3.1.1 公平性 32
3.1.2 最终性 33
3.2 时序Petri网 33
3.2.1 形式定义 33
3.2.2 性质分析 35
3.3 时序高级Petri网 36
3.3.1 时序有色Petri网 36
3.3.2 时序谓词／变迁网 37
3.4 案例分析 38
3.4.1 一个网上证券交易系统 38
3.4.2 证券交易系统的时序Petri网模拟与分析 41
3.4.3 证券交易系统的时序有色Petri网模拟与分析 49
3.4.4 证券交易系统的时序谓词／变迁网模拟与分析 56
第四章 批处理功能及传值不确定性分析 59
4.1 批处理功能 59
4.2 传值不确定性 60
4.3 逻辑Petri网（LPN） 61
4.3.1 形式定义 61
4.3.2 逻辑Petri网与PN和HLPN之间的关系 63
4.4 逻辑工作流网 64
4.4.1 形式定义 64
4.4.2 构造算法 65
4.4.3 逻辑工作流网的性质 65
4.5 组织间逻辑工作流网及其性质 69
第五章 实时性质模拟与验证技术 72
5.1 电子商务系统的实时性质 72
5.2 逻辑时间Petri网 72
5.2.1 时间Petri网的时序公式语义 73
5.2.2 形式定义 73
5.2.3 LTPN与TPN和有色TPN的比较 75
5.3 逻辑时间工作流网 77
5.3.1 形式定义 77
5.3.2 性质分析 78
5.4 组织间逻辑时间工作流网 80
5.4.1 形式定义 80
5.4.2 ILTWfN的健壮性分析 81
第六章 主体责任及证据模拟分析 86
6.1 主体责任 86
6.2 不可否认与证据 87
6.3 标注Petri网 87
6.3.1 一个简单的电子采购系统 87
6.3.2 形式定义 89
6.4 标注工作流网 92
6.4.1 形式定义 92
6.4.2 健壮性和无阻塞性 93
6.5 组织间标注工作流网 94
6.5.1 形式定义 94
6.5.2 性质分析 95
6.6 责任与证据的形式分析 99
6.6.1 责任分析 99
6.6.2 证据 100
6.7 应用实例 101
6.7.1 IOTP购买交易 102
6.7.2 购买交易的标注工作流网模型 103
6.7.3 购买交易性质分析 107
第七章 总结和展望 110
7.1 本文总结 110
7.2 进一步的研究工作 111
参考文献 112
附录一 读博士期间发表的学术论文 120
附录二 读博士期间承担科研项目及获奖情况 121
附录三 读博士期间参加国际国内学术会议情况 122
致谢 123