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

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

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

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

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

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

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