面向自動(dòng)化模型檢測(cè)的模型提取工具的設(shè)計(jì)與實(shí)現(xiàn).pdf

1、隨著計(jì)算機(jī)軟件日益復(fù)雜，如何保證其正確性和可靠性成為十分緊迫的問題。模型檢測(cè)是一種驗(yàn)證有限狀態(tài)系統(tǒng)的時(shí)序邏輯屬性的形式化方法，已經(jīng)在硬件電路、驅(qū)動(dòng)程序和安全協(xié)議等領(lǐng)域獲得了巨大的成功。 應(yīng)用模型檢測(cè)技術(shù)到高級(jí)程序設(shè)計(jì)語言實(shí)現(xiàn)的系統(tǒng)的難點(diǎn)是提取抽象模型，通常的辦法是手工構(gòu)造。然而這個(gè)方法存在一些不足，如成本過高，易引入建模錯(cuò)誤等，因此從源代碼中直接提取驗(yàn)證模型存在強(qiáng)烈的實(shí)際需求。貝爾實(shí)驗(yàn)室開發(fā)的SPIN是優(yōu)秀的模型檢測(cè)工具，其建模

2、語言是PROMELA，而C語言是應(yīng)用最廣泛的程序設(shè)計(jì)語言之一，因此本文的主要研究內(nèi)容定位于ANSI-C程序的模型提取技術(shù)，從而達(dá)到使用SPIN自動(dòng)化模型檢測(cè)C程序的目的。 本文設(shè)計(jì)了一套對(duì)ANSI-C程序進(jìn)行模型提取的方法，較好地處理了C的大部分語言特性，特別是幾種復(fù)雜的結(jié)構(gòu)，比如遞歸函數(shù)、枚舉類型和指針等。并開發(fā)了一個(gè)模型提取工具C2Spin。從功能上來說，C2Spin分為前端和后端。前端是一個(gè)分析器，具有對(duì)C源代碼進(jìn)行詞法分

3、析和語法分析的功能。后端則是一個(gè)轉(zhuǎn)換器，實(shí)現(xiàn)了從C代碼到PROMELA代碼的系統(tǒng)轉(zhuǎn)換。而且，為了減小模型的規(guī)模，加快模型提取的速度或者提高模型的執(zhí)行效率，C2Spin中使用了一些簡單的抽象機(jī)制和優(yōu)化技術(shù)。 C2Spin顯著降低了建模的開銷。結(jié)合C2Spin，SPIN能夠自動(dòng)地檢測(cè)使用C語言編寫的應(yīng)用程序中的多種錯(cuò)誤，比如死鎖等性質(zhì)。作者使用C2Spin進(jìn)行了一定數(shù)量的測(cè)試。在實(shí)驗(yàn)中，依靠C2Spin生成的模型，我們發(fā)現(xiàn)了SPI