鐵路信號(hào)系統(tǒng)中聯(lián)鎖軟件形式化描述方法的研究.pdf

1、鐵路聯(lián)鎖軟件是一種典型的安全性軟件,其失效可能會(huì)帶來(lái)大批生命財(cái)產(chǎn)的損失或嚴(yán)重的環(huán)境破壞.在目前通用的軟件開(kāi)發(fā)方法中,其描述通常是用非形式化的圖和文本,不能描述系統(tǒng)期望的存在于構(gòu)件之間的接口,不能描述不同的組成系統(tǒng)的組合關(guān)系,難以被開(kāi)發(fā)人員理解,更不能用來(lái)分析其一致性和完整性等特性.采用形式化方法為鐵路聯(lián)鎖軟件規(guī)則建模可以成為解決以上問(wèn)題的入手點(diǎn),在保證軟件安全性和可靠性方面,也有很重要的意義. 本文的研究對(duì)象是由合肥工業(yè)大學(xué)開(kāi)發(fā)

2、的"HJ04A鐵路信號(hào)計(jì)算機(jī)聯(lián)鎖系統(tǒng)".其主要內(nèi)容是對(duì)聯(lián)鎖軟件規(guī)則進(jìn)行形式化描述并進(jìn)行比較分析,找到更適合描述聯(lián)鎖軟件規(guī)則的形式化方法,即時(shí)間自動(dòng)機(jī),利用UPPAAL實(shí)時(shí)驗(yàn)證工具進(jìn)行建模和驗(yàn)證. 論文在充分了解了計(jì)算機(jī)聯(lián)鎖軟件的背景和現(xiàn)狀的情況下,提出了形式化方法在鐵路信號(hào)系統(tǒng)聯(lián)鎖軟件需求分析階段具有重要的作用.然后介紹了形式化方法的概念和幾種常見(jiàn)的形式化方法的定義和原理,接著介紹了鐵路信號(hào)的相關(guān)概念、計(jì)算機(jī)聯(lián)鎖軟件規(guī)則,并利用