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

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

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

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