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

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

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