一類對象Petri網(wǎng)建模與驗證方法研究.pdf

1、Petri網(wǎng)是一種既有直觀的圖形表示方式，又有嚴格數(shù)學(xué)理論基礎(chǔ)和多種分析方法的建模工具。使用Petri網(wǎng)的分析方法可以刻畫系統(tǒng)的結(jié)構(gòu)，展現(xiàn)系統(tǒng)的運行機制，表示和分析系統(tǒng)的動態(tài)行為。帶有對象的Petri網(wǎng)(PNO)是將面向?qū)ο蠓椒ê椭^詞/變遷網(wǎng)有機結(jié)合而定義的一種高級Petri網(wǎng)。因為PNO在初始化和驗證具體系統(tǒng)時才構(gòu)建庫所的標識關(guān)系，變遷的使能與對象狀態(tài)相關(guān)，并且變遷的實施需要修改托肯和相關(guān)對象的屬性，因此不便于直接使用常規(guī)的分析技術(shù)驗

2、證PNO模型。 針對PNO模型存在的分析驗證問題，本文將時態(tài)邏輯引入PNO模型，提出了相應(yīng)的建模及驗證方法。建模方法使用精確標識PNO描述系統(tǒng)體系結(jié)構(gòu)模型，并通過時態(tài)邏輯定義模型上的需求和限制。驗證方法使用SMV工具驗證PNO模型和時態(tài)邏輯之間的一致性，該方法包括三個步驟。首先，根據(jù)SMV的要求在模型中增加與變遷有關(guān)的對象屬性，并根據(jù)增加的對象屬性細化變遷附加條件函數(shù)和變遷實施處理函數(shù)。其次，使用時態(tài)邏輯公式描述系統(tǒng)的屬性。最后