總序
論叢前言
前言
第1章 緒論
1.1 電子商務
1.1.1 電子商務定義
1.1.2 電子商務系統(tǒng)體系
1.2 電子商務系統(tǒng)的特點
1.3 工作流管理系統(tǒng)
1.3.1 基本概念
1.3.2 體系結構
1.3.3 電子商務中的工作流
1.4 電子商務系統(tǒng)形式化技術綜述
1.4.1 一般形式化方法
1.4.2 基于邏輯的方法
1.4.3 基于Petri網的方法
1.4.4 基于工作流網的方法
1.4.5 四類形式化方法比較及本書工作的重要性
1.5 約定和假設
1.6 本書的研究動機和貢獻
1.6.1 研究動機
1.6.2 主要研究內容
1.6.3 主要貢獻
第2章 基本知識
2.1 Petri網(PN)
2.1.1 Petri網概念
2.1.2 Petri網性質
2.1.3 謂詞/變遷(Pr/T)網
2.1.4 有色Petri網((2PN)
2.1.5 時間Petri網(TPN)
2.2 時序邏輯
2.2.1 基本概念
2.2.2 時序邏輯系統(tǒng)
2.3 工作流網
2.3.1 形式定義
2.3.2 工作流網性質
第3章 電子商務系統(tǒng)時序性質分析與驗證
3.1 時序性質
3.1.1 公平性
3.1.2 最終性
3.2 時序Petri網
3.2.1 形式定義
3.2.2 性質分析
3.3 時序高級Petri網
3.3.1 時序有色Petri網
3.3.2 時序謂詞/變遷網
3.4 案例分析
3.4.1 一個網上證券交易系統(tǒng)
3.4.2 證券交易系統(tǒng)的時序Petri網模擬與分析
3.4.3 證券交易系統(tǒng)的時序有色Petri網模擬與分析
3.4.4 證券交易系統(tǒng)的時序謂詞/變遷網模擬與分析
第4章 批處理功能及傳值不確定性分析
4.1 批處理功能
4.2 傳值不確定性
4.3 邏輯Petri網(LPN)
4.3.1 形式定義
4.3.2 邏輯Petri網與PN和HLPN之間的關系
4.4 邏輯工作流網
4.4.1 形式定義
4.4.2 構造算法
4.4.3 邏輯工作流網的性質
4.5 組織間邏輯工作流網及其性質
第5章 實時性質模擬與驗證技術
5.1 電子商務系統(tǒng)的實時性質
5.2 邏輯時間Petri網
5.2.1 時間Petri網的時序公式語義
5.2.2 形式定義
5.2.3 LTPN與TPN和有色TPN的比較
5.3 邏輯時間工作流網
5.3.1 形式定義
5.3.2 性質分析
5.4 組織間邏輯時間工作流網
5.4.1 形式定義
5.4.2 ILTWfN的健壯性分析
第6章 主體責任及證據模擬分析
6.1 主體責任
6.2 不可否認與證據
6.3 標注Petri網
6.3.1 一個簡單的電子采購系統(tǒng)
6.3.2 形式定義
6.4 標注工作流網
6.4.1 形式定義
6.4.2 健壯性和無阻塞性
6.5 組織間標注工作流網
6.5.1 形式定義
6.5.2 性質分析
6.6 責任與證據的形式分析
6.6.1 責任分析
6.6.2 證據
6.7 應用實例
6.7.1 IOTP購買交易
6.7.2 購買交易的標注工作流網模型
6.7.3 購買交易性質分析
第7章 總結和展望
7.1 本書總結
7.2 進一步的研究工作
參考文獻
后記