電子商務系統(tǒng)的Petri網建模理論與分析技術研究.pdf

1、電子商務已成為Internet的重要應用之一。然而，隨著用戶數量的增加和服務類型的多樣化，電子商務系統(tǒng)愈來愈龐大、愈來愈復雜，這使得電子商務系統(tǒng)的設計和分析更加困難。一般情況下，電子商務系統(tǒng)的需求規(guī)范采用非形式化方式描述，且這種描述具有二義性。本文應用形式化方法對電子商務系統(tǒng)進行模擬與驗證，能夠為系統(tǒng)設計者提供一種既明確又便于理解和掌握的系統(tǒng)整體架構，幫助設計者查找系統(tǒng)設計中的漏洞或缺陷，驗證系統(tǒng)的活性、安全性、公平性和正確

2、性等動態(tài)行為性質，使其更加規(guī)范、有效、合理、因此，本文的研究工作具有重要的理論價值和實際意義。本文在對大量現有電子商務系統(tǒng)形式化方法分析的基礎上，根據電子商務系統(tǒng)的具體特點，綜合應用Petri網、時序邏輯、工作流等分析技術，提出并研究了用于電子商務系統(tǒng)時序性質分析的時序(高級)Petri網方法、批處理功能及傳值不確定性分析的邏輯工作流網方法、實時性質分析的邏輯時間工作流網方法和主體責任與證據分析的標注工作流網方法。同時，從理

3、論上研究了這些方法的主要性質，得到一系列重要結果。通過對案例分析，例證了它們在電子商務系統(tǒng)分析中的應用價值。目前，國內外可應用于電子商務系統(tǒng)形式描述與驗證的方法主要分為四大類：一般形式化方法、基于邏輯的形式化方法、基于Petri網的形式化方法和基于工作流網的形式化方法。它們?yōu)殡娮由虅盏陌l(fā)展和應用起了重要的促進作用。本文綜合分析了它們的特點和缺陷，并在它們的啟發(fā)下，提出并研究了幾種用于電子商務系統(tǒng)不同性質形式化分析的有效方法

4、。與現有電子商務系統(tǒng)形式化方法相比較，本文工作的主要貢獻表現在如下幾個方面：(1)首次將時序Petri網應用于電子商務系統(tǒng)的時序性質分析，且提出并研究了時序高級(有色、謂詞/變遷)Petri網分析技術。以網上證券交易系統(tǒng)為例，具體例證了時序Petri網和時序高級Petri網模擬與驗證技術在電子商務系統(tǒng)中的應用價值，并基于它的Petri網模型，分析了證券交易系統(tǒng)的時序性質和功能正確性。(2)電子商務系統(tǒng)中的批處理功能，涉及傳

5、值不確定性。在電子商務系統(tǒng)批處理功能及傳值不確定性形式化分析技術研究方面，本文工作具有一定突破。本文提出的邏輯工作流網分析技術，既能描述與分析電子商務系統(tǒng)的一般性質，又能夠極好地模擬與驗證電子商務系統(tǒng)的批處理功能和傳值不確定性。(3)傳統(tǒng)的實時協(xié)同系統(tǒng)分析方法，不能明確描述與驗證系統(tǒng)的批處理功能和傳值不確定性。本文提出的邏輯時間工作流網，既能分析電子商務系統(tǒng)的實時性質，叉能描述與驗證系統(tǒng)的批處理功能及傳值不確定性。(4)在

6、電子商務系統(tǒng)主體責任、不可否認性及證據的形式化表達與分析方面，本文克服形式語言方法過于抽象、不便于設計者理解等缺點，提出并研究了標注工作流網分析技術。它能夠充分利用Petri網的動態(tài)可視特性和工作流網的完善分析技術，明確描述和分析電子商務系統(tǒng)中的主體責任、不可否認性與證據。同時，我們將無阻塞理論引入標注工作流網中，使工作流網的模擬與分析能力進一步增強，其健壯性分析技術更加完善。關鍵詞：電子商務系統(tǒng)，實時性質，安全性，時序性質