嵌入式軟件瞬時故障的形式驗證方法研究及實現(xiàn).pdf

1、在現(xiàn)代社會中，軟件扮演著一個非常重要的角色，廣泛應(yīng)用到各種領(lǐng)域。軟件誕生一來，軟件安全問題也隨之產(chǎn)生。長期以來人們對軟件的安全性問題重視不夠，致使軟件存在一定的潛在風(fēng)險，有的甚至導(dǎo)致重大的災(zāi)難。嵌入式軟件廣泛應(yīng)用于航空航天，軍事，衛(wèi)星，核反應(yīng)實驗等特殊軟件應(yīng)用領(lǐng)域，它們對軟件的可靠性要求更高。因為在這些領(lǐng)域的嵌入式軟件，很容易受到外界的高能粒子的干擾，引起錯誤。瞬時故障是導(dǎo)致嵌入式軟件發(fā)生錯誤的一個主要原因，本文針對這種故障進(jìn)行了研究。

2、
　　本文基于類型化匯編語言和Hoare邏輯，研究了一種針對嵌入式軟件瞬時故障的容錯方法，并形式化地證明了該容錯方法的正確性。該容錯方案是一種軟硬結(jié)合的解決方案，在硬件方面需要對硬件進(jìn)行特殊的設(shè)計以支持軟件，在軟件方面采用兩冗余程序，兩份程序執(zhí)行相同的操作，但在某些指令上略有不同。
　　為了硬件能夠檢測出瞬時故障，建立了抽象的機(jī)器模型。機(jī)器模型說明了所討論范圍內(nèi)的瞬時故障模型，類型化匯編語言的語法，指令的操作語義以及為實現(xiàn)故