【摘要】：針對現(xiàn)行建模方法不能滿足鐵路信號系統(tǒng)安全關鍵軟件的時鐘約束需求和模型復雜度較高的問題,分析SyncCharts建模方法,針對其缺少形式化規(guī)范和時鐘約束的問題,擴展出具有時鐘屬性的Timed SyncCharts建模方法。首先,采用Z語言系統(tǒng)地給出了Timed SyncCharts的形式化定義;其次,結合Timed SyncCharts的組件元素,確定Timed SyncCharts的宏步轉(zhuǎn)移機制;然后,提出將Timed SyncCharts轉(zhuǎn)化為Kripke結構的規(guī)則,保證了模型分析的可行性;最后,建立計算機聯(lián)鎖軟件道岔定位需求的Timed SyncCharts模型,證明該方法的可行性和有效性。
[Abstract]:Aiming at the problem that the current modeling method can not meet the requirement of clock constraint and the high complexity of the model of the key software of railway signal system security, this paper analyzes the SyncCharts modeling method, aiming at the lack of formal specification and clock constraint. The Timed SyncCharts modeling method with clock attribute is extended. Firstly, the formal definition of Timed SyncCharts is given systematically by using Z language, secondly, the macro step transfer mechanism of Timed SyncCharts is determined by combining the component elements of Timed SyncCharts. Then, the rules of transforming Timed SyncCharts into Kripke structure are proposed to ensure the feasibility of model analysis. Finally, the Timed SyncCharts model of computer interlocking software switch location requirements is established to prove the feasibility and effectiveness of the method.
【作者單位】： 西南交通大學信息科學與技術學院;
【基金】：中國鐵路總公司重點項目(2015X009-D;2014X008-A)
【分類號】：TP309;U284.95

【相似文獻】

相關期刊論文 前10條

1 張利;懷柔站西門子計算機聯(lián)鎖技術通過審查[J];鐵道通信信號;2000年01期

2 宋西欣;計算機聯(lián)鎖設備維修體制探討[J];鐵道通信信號;2000年10期

3 嚴黎,吳芳美;鐵路車站計算機聯(lián)鎖軟件的安全性評估策略[J];同濟大學學報(自然科學版);2002年09期

4 夏平,朱楚生;計算機聯(lián)鎖設備的推廣與應用[J];中國鐵路;2002年07期

5 王歷江;計算機聯(lián)鎖設備在我局應用的經(jīng)濟技術指標分析及建議[J];哈爾濱鐵道科技;2002年01期

6 郭東福,段國強,李軍;津霸線車站計算機聯(lián)鎖的問題分析與解決[J];鐵道通信信號;2003年07期

7 張清顯,于華都;計算機聯(lián)鎖換型改造的施工[J];鐵道通信信號;2003年07期

8 嚴大龍,季忠洪;計算機聯(lián)鎖電源系統(tǒng)有關問題的分析及改進[J];鐵道通信信號;2003年11期

9 酈萌,徐翥,王鐵江;計算機聯(lián)鎖軟件制式的安全性評價[J];鐵道學報;2004年01期

10 張樹坤;計算機聯(lián)鎖過渡施工新方法[J];鐵道通信信號;2004年03期

相關會議論文 前5條

1 張飛寧;;對于計算機聯(lián)鎖進一步發(fā)展的思考[A];《河南鐵道》2011年第5期[C];2011年

2 袁于思;;集二鐵路集寧至賁紅段區(qū)域計算機聯(lián)鎖方案[A];中國電氣化鐵路兩萬公里學術會議論文集[C];2005年

3 潘明;何梅芳;張萍;趙陽;趙永青;;計算機聯(lián)鎖安全電子終端及其冗余組態(tài)的研究[A];鐵道科學技術新進展——鐵道科學研究院五十五周年論文集[C];2005年

4 胡忠康;陳辛怡;;計算機聯(lián)鎖設備外部混線故障案例分析[A];浙江省鐵道學會2006年學術交流會論文集[C];2006年

5 楊曉強;;對計算機聯(lián)鎖軌道采集電路引發(fā)故障的分析及措施[A];《河南鐵道》2011年第5期[C];2011年

相關博士學位論文 前1條

1 陳永;基于高可信無線通信的列車流形式化建模與仿真[D];蘭州交通大學;2014年

相關碩士學位論文 前10條

1 劉培頂;計算機聯(lián)鎖安全輸入/輸出板編程器的設計與開發(fā)[D];西南交通大學;2015年

2 劉濤;區(qū)域計算機聯(lián)鎖站間安全通信的研究[D];蘭州交通大學;2015年

3 牛凱蘭;晨曦火車站聯(lián)鎖控制模擬系統(tǒng)的設計與實現(xiàn)[D];電子科技大學;2015年

4 侯宇婷;基于安全狀態(tài)機的計算機聯(lián)鎖系統(tǒng)建模與分析[D];西南交通大學;2016年

5 張京晶;基于UML的鐵路信號計算機聯(lián)鎖仿真系統(tǒng)的研究與實現(xiàn)[D];北京工業(yè)大學;2016年

6 姚文韜;高鐵計算機聯(lián)鎖仿真培訓系統(tǒng)—聯(lián)鎖軟件的研究[D];蘭州交通大學;2016年

7 蘇琛;高鐵計算機聯(lián)鎖教學培訓子系統(tǒng)研究[D];蘭州交通大學;2016年

8 薛豐;計算機聯(lián)鎖自動測試系統(tǒng)研究與設計[D];西南交通大學;2017年

9 馮濤;網(wǎng)絡計算機聯(lián)鎖仿真系統(tǒng)研究[D];蘭州交通大學;2013年

10 韓海玲;全電子計算機聯(lián)鎖軟件質(zhì)量度量分析與研究[D];蘭州交通大學;2013年

，

本文編號：2407885