基于時間有色Petri網(wǎng)的聯(lián)鎖軟件的形式化建模與分析.pdf

1、在眾多計算機應(yīng)用領(lǐng)域中，鐵路車站聯(lián)鎖系統(tǒng)不僅是實時系統(tǒng)，而且還是安全一關(guān)鍵系統(tǒng)。這種系統(tǒng)和航天、核工業(yè)、軍事等應(yīng)用系統(tǒng)具有一個重要的共同特征，就是它們的正確運行與否關(guān)系到人的生命安危和大量財產(chǎn)損失或生態(tài)環(huán)境的破壞。這種系統(tǒng)的時間參量非常重要，但是系統(tǒng)運行是否安全更關(guān)鍵。因此，在計算機技術(shù)和智能控制技術(shù)得到充分發(fā)展和應(yīng)用的今天，對鐵路車站聯(lián)鎖系統(tǒng)進行完備的形式化描述越來越受到重視?，F(xiàn)有對鐵路車站聯(lián)鎖系統(tǒng)的形式化描述工具主要是petri網(wǎng)和

2、擴展petri網(wǎng)相關(guān)技術(shù)。但是現(xiàn)有技術(shù)大多數(shù)限于滿足邏輯的準(zhǔn)確性及模型的簡化，添加時間約束的建模和模型分析還鮮見報道。 本文主要研究鐵路車站聯(lián)鎖系統(tǒng)的形式化建模和模型分析。在現(xiàn)有的時間petri網(wǎng)模型和有色petri網(wǎng)模型基礎(chǔ)上，結(jié)合區(qū)間時間有色petri網(wǎng)(IntervalTimed Colored Petri Nets，簡稱ITCPN)對鐵路車站聯(lián)鎖邏輯進行建模和模型分析。ITCPN使模型更接近實際系統(tǒng)(加入運行時間區(qū)間，即