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

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

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

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

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

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

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