基于PVS對SCADE開發(fā)軌交控制系統(tǒng)的形式化建模與驗(yàn)證.pdf

1、隨著計算機(jī)微處理器技術(shù)的迅速發(fā)展，嵌入式系統(tǒng)的設(shè)計越來越復(fù)雜。特別是對于安全性要求極高的系統(tǒng)，例如飛機(jī)，火箭，軌道列車控制系統(tǒng)等等。設(shè)計中的任何細(xì)小的缺陷都有可能造成災(zāi)難性后果，并造成巨大的經(jīng)濟(jì)損失。因此，研究如何設(shè)計出高可信的嵌入式系統(tǒng)是非常重要的。
　　 軌交控制系統(tǒng)對可靠性要求是非常高的，單單傳統(tǒng)的驗(yàn)證方法已經(jīng)不能滿足要求，需要提出新的建模與驗(yàn)證方法來完成其開發(fā)設(shè)計。為此本文提出了一種基于PVS(原型驗(yàn)證系統(tǒng))對SCADE

2、開發(fā)軌交控制系統(tǒng)的形式化建模與驗(yàn)證的方法。研究以SCADE Suite作為開發(fā)工具的圖形化建模方式和由SCADE Suite生成的圖形模型自動轉(zhuǎn)換的Lustre語言。在此基礎(chǔ)上，對于基本Lustre語言，包括constants常量、variable變量、condition條件語句、special operator特殊操作符等給出在PVS中的轉(zhuǎn)換規(guī)則，對于擴(kuò)展Lustre語言狀態(tài)描述的部分，則給出了對其轉(zhuǎn)換的基本策略。在SCADE Sui

3、te建立模型的基礎(chǔ)上，根據(jù)SCADE轉(zhuǎn)換至PVS的規(guī)則，逐行讀取建模后所生成的代碼，并將之轉(zhuǎn)換成PVS的相應(yīng)理論，通過Ruby腳本語言，設(shè)計并實(shí)現(xiàn)了由Lustre語言到PVS轉(zhuǎn)換工具，SCADE2PVS。在SCADE Suite建立模型的基礎(chǔ)上，根據(jù)SCADE轉(zhuǎn)換至PVS的規(guī)則，逐行讀取建模后所生成的每一行代碼，并將之轉(zhuǎn)換成PVS的相應(yīng)理論。
　　 最后通過軌道交通控制系統(tǒng)中的列車道岔換軌例子說明了該方法的可行性，闡述了通過SC