1、在城市軌道交通信號系統(tǒng)中，聯(lián)鎖系統(tǒng)是保證行車安全的重要設(shè)備，同樣也是安全關(guān)鍵系統(tǒng)，必須滿足安全完整性等級SIL-4級安全需求，它直接關(guān)系到人民的生命和財產(chǎn)安全。利用傳統(tǒng)的開發(fā)方法設(shè)計并開發(fā)聯(lián)鎖系統(tǒng)，難度高且不易尋找錯誤和安全隱患，基于模型的軟件開發(fā)方法在安全關(guān)鍵領(lǐng)域逐漸被接受。高安全性應(yīng)用開發(fā)環(huán)境（Safety Critical Application Development Environment，SCADE），為高安全性系統(tǒng)的軟件開

2、發(fā)提供了一套基于模型的嵌入式軟件開發(fā)的方案，可以減少軟件開發(fā)風(fēng)險，縮短驗證時間，降低開發(fā)成本。但安全屬性的難以表達以及安全模型的龐大，給驗證和安全分析工作帶來困難。本文基于SCADE對移動閉塞下的聯(lián)鎖功能模型進行搭建，為保證系統(tǒng)安全性，提出基于故障樹分析(Fault Tree Analysis，F(xiàn)TA)的SCADE聯(lián)鎖功能模型安全性分析與驗證方法。
　　論文主要工作有:
　　(1)分析城軌聯(lián)鎖系統(tǒng)結(jié)構(gòu)與功能需求，研究移動閉塞

3、下特殊進路以及對進路控制過程的要求。實現(xiàn)聯(lián)鎖功能模塊概要設(shè)計，根據(jù)進路狀態(tài)，將進路控制功能模塊劃分為選路模塊、選排一致檢查模塊、進路檢查模塊、信號開放模塊、接近鎖閉模塊、正常解鎖模塊以及取消進路模塊;
　　(2)基于SCADE對聯(lián)鎖功能模塊進行設(shè)計并建模，完成了移動閉塞下進路控制功能模塊的建模，在正線進路控制的基礎(chǔ)上，實現(xiàn)了對多列車進路、折返進路、自動進路以及保護進路的控制;
　　(3)結(jié)合SCADE形式化驗證過程，提出了基

4、于故障樹的SCADE聯(lián)鎖功能模型安全分析與驗證方法，搭建了SCADE環(huán)境下聯(lián)鎖模型的驗證框架?；贔TA分析聯(lián)鎖功能模型的安全性，構(gòu)建功能模型的故障樹模型，將其作為安全特性模型進行形式化驗證;
　　(4)提出基于失效模式與影響分析(Failure Modes and Effect Analysis，F(xiàn)MEA)搭建聯(lián)鎖功能模型故障樹的方法，構(gòu)建了進路控制功能模塊的故障樹;以進路建立過程為例，搭建故障樹模型，分析進路建立功能模型的安全