一類(lèi)對(duì)象Petri網(wǎng)建模與驗(yàn)證方法研究.pdf

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

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