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

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

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

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