安全C語(yǔ)言程序驗(yàn)證器中驗(yàn)證條件生成器的擴(kuò)展設(shè)計(jì)與實(shí)現(xiàn).pdf

1、交通、電力、軍事等關(guān)鍵領(lǐng)域?qū)浖目煽啃院桶踩砸笤絹?lái)越高，因?yàn)槠鋰?yán)重關(guān)乎國(guó)民的人身和財(cái)產(chǎn)安全。C語(yǔ)言在上述基礎(chǔ)領(lǐng)域軟件的開(kāi)發(fā)中有廣泛的應(yīng)用。C語(yǔ)言靈活高效的特性允許程序員做相當(dāng)?shù)讓拥牟僮鳎矊?dǎo)致C程序容易出現(xiàn)非法指針解引用、內(nèi)存泄漏、緩沖區(qū)溢出等缺陷。
　　形式化驗(yàn)證是一種可以嚴(yán)格保證程序可靠性的方法。本課題組正在研發(fā)一個(gè)安全C語(yǔ)言驗(yàn)證器，其功能是對(duì)攜有程序標(biāo)注的安全C語(yǔ)言程序進(jìn)行演繹推理，驗(yàn)證程序是否滿足預(yù)期規(guī)范。

2、　　安全C語(yǔ)言驗(yàn)證器中驗(yàn)證條件生成器的作用是支持安全C語(yǔ)言和規(guī)范語(yǔ)言SCSL的語(yǔ)法，實(shí)現(xiàn)每條語(yǔ)句的演算規(guī)則，并根據(jù)演算規(guī)則遍歷源程序進(jìn)行演算，同時(shí)產(chǎn)生程序點(diǎn)的斷言和合理有效的驗(yàn)證條件。本文的工作是對(duì)安全C語(yǔ)言驗(yàn)證器中的驗(yàn)證條件生成器進(jìn)行擴(kuò)展。
　　本文的主要工作和貢獻(xiàn)如下:
　　第一、參與規(guī)范語(yǔ)言SCSL中邏輯變量、幽靈代碼、字符串類型、帶命名行為協(xié)議和多函數(shù)協(xié)議的設(shè)計(jì)，提高了規(guī)范語(yǔ)言的表達(dá)能力，同時(shí)獨(dú)立設(shè)計(jì)和實(shí)現(xiàn)了對(duì)應(yīng)的演

3、算規(guī)則。
　　第二、基于Hoare邏輯設(shè)計(jì)和實(shí)現(xiàn)跳轉(zhuǎn)語(yǔ)句goto、continue和break、選擇語(yǔ)句switch以及函數(shù)調(diào)用語(yǔ)句的演算規(guī)則，使得驗(yàn)證器可以支持更多C的語(yǔ)法和控制結(jié)構(gòu)，擴(kuò)大了驗(yàn)證器的適用范圍。同時(shí)實(shí)現(xiàn)了賦值語(yǔ)句前對(duì)全稱量化斷言和謂詞的展開(kāi)，減輕了自動(dòng)定理證明器的負(fù)擔(dān)。
　　第三、根據(jù)C語(yǔ)言的語(yǔ)義提出了一種適用于程序驗(yàn)證的棧區(qū)內(nèi)存模型，可以支持結(jié)構(gòu)體和多級(jí)指針等數(shù)據(jù)類型，并基于該模型實(shí)現(xiàn)了取地址、多級(jí)解引用和