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

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

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