基于時間有色Petri網的聯鎖軟件的形式化建模與分析.pdf

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

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