一類對象Petri網建模與驗證方法研究.pdf

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

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