計(jì)算機(jī)聯(lián)鎖安全關(guān)鍵軟件可靠性設(shè)計(jì).pdf

1、隨著3C技術(shù)(計(jì)算機(jī)技術(shù)、通信技術(shù)、控制技術(shù))的不斷發(fā)展和計(jì)算機(jī)聯(lián)鎖技術(shù)的成熟，鐵路行業(yè)越來越多地使用計(jì)算機(jī)聯(lián)鎖來替代電氣集中控制。鐵路運(yùn)輸涉及到人身安全和財(cái)產(chǎn)損失，對(duì)安全性和可靠性的要求十分高，這就對(duì)計(jì)算機(jī)聯(lián)鎖的安全性和可靠性提出了很高的要求，計(jì)算機(jī)聯(lián)鎖軟件一旦失效將會(huì)造成重大的生命財(cái)產(chǎn)損失。如何提高計(jì)算機(jī)聯(lián)鎖軟件的安全性和可靠性，成為了計(jì)算機(jī)聯(lián)鎖設(shè)計(jì)者們不斷思考和研究的課題。
　　為了提高計(jì)算機(jī)聯(lián)鎖軟件的安全性和可靠性，開發(fā)者

2、們必須在軟件開發(fā)的前期對(duì)軟件的可靠性進(jìn)行分析和驗(yàn)證。通常在軟件開發(fā)前期，對(duì)軟件進(jìn)行建模，并對(duì)模型進(jìn)行驗(yàn)證。常用的建模方式有結(jié)構(gòu)化建模、形式化建模、面向?qū)ο蟮慕?、UML建模等，各個(gè)建模方法各有其優(yōu)缺點(diǎn)，本論文主要采用形式化建模方法。對(duì)于結(jié)構(gòu)化方法等利用自然語(yǔ)言對(duì)軟件建立的模型，由于自然語(yǔ)言可能存在的二義性，容易使開發(fā)者的理解出現(xiàn)偏差，會(huì)給軟件的后期開發(fā)帶來嚴(yán)重的問題。而形式化方法是用數(shù)學(xué)語(yǔ)言來描述模型，具有結(jié)構(gòu)嚴(yán)謹(jǐn)、無二義性等優(yōu)點(diǎn)，便于

3、實(shí)現(xiàn)設(shè)計(jì)，同時(shí)也可以提高軟件的可靠性。
　　petri網(wǎng)是一種常用形式化建模方法，具有直觀易懂的優(yōu)點(diǎn)。通過對(duì)軟件需求和規(guī)則的分析之后，用petri網(wǎng)建立它的數(shù)學(xué)模型，并用petri網(wǎng)獨(dú)有的驗(yàn)證方法對(duì)其分析驗(yàn)證，為開發(fā)人員及時(shí)發(fā)現(xiàn)軟件的缺陷提供了極大的幫助。本論文采用CPN(有色petri網(wǎng))對(duì)計(jì)算機(jī)聯(lián)鎖軟件進(jìn)行建模和分析。CPN可以對(duì)模擬量系統(tǒng)和離散量系統(tǒng)建模，有色 petri網(wǎng)給不同屬性的托肯染上不同的顏色，在有色 petri網(wǎng)

4、中用一種染色的托肯來代表一種行為特征。它的顏色集可以是離散值或者連續(xù)值。對(duì)建立的模型可以用 CPN專門的仿真工具CPN TOOLS進(jìn)行仿真，以此來分析所建模型是否存在死鎖等性質(zhì)。
　　本論文首先介紹了計(jì)算機(jī)聯(lián)鎖系統(tǒng)的結(jié)構(gòu)、功能，以及計(jì)算機(jī)聯(lián)鎖軟件可靠性的設(shè)計(jì)要求，提出了用形式化方法對(duì)計(jì)算機(jī)聯(lián)鎖軟件進(jìn)行建模的優(yōu)越性。然后介紹了形式化建模語(yǔ)言petri網(wǎng)的定義和建模方法。接著采用CPN對(duì)計(jì)算機(jī)聯(lián)鎖軟件中的主要設(shè)備道岔、軌道區(qū)段、信號(hào)機(jī)