制造系統(tǒng)結(jié)構(gòu)化控制—基于Petri網(wǎng)的模型驗證方法.pdf

1、該文利用模型驗證(Model-Checking)方法的強大運算能力,這篇文章給出一個新的制造系統(tǒng)的結(jié)構(gòu)化控制器,該控制器利用符合模型驗證(Symbolic Model Checking)方法來驗證系統(tǒng)行為的正確性.一種名為Petri網(wǎng)的離散事件系統(tǒng)模型被用來描述系統(tǒng)動態(tài)行為.系統(tǒng)的資源用庫所表示,系統(tǒng)可以執(zhí)行的任務(wù)往往需要一系列的資源被依次分配給它,這一過程用一組庫所、變遷依次交替的Petri網(wǎng)來表達,并且這些變遷與系統(tǒng)資源庫所交互.結(jié)

2、構(gòu)化控制器希望控制的系統(tǒng)性質(zhì),采用時態(tài)邏輯描述.作為一個示例,一個符合模型驗證工具SMV被用來作為結(jié)構(gòu)化控制器的運算工具.每當(dāng)系統(tǒng)進入一個新狀態(tài),該控制器檢測所有可行的變遷,一個變遷被觸發(fā),僅當(dāng)其發(fā)生后的系統(tǒng)狀態(tài)滿足期望的時態(tài)邏輯公式.一些已有的死鎖避免算法被納入這個結(jié)構(gòu)化控制器框架.這些控制算法被時態(tài)邏輯重新表示,并且,模型驗證方法使得其運算更為有效.此外,文中還討論了對于不可靠資源情形下的死鎖避免問題.通過一些例子,展示了這個結(jié)構(gòu)化