基于程序切片的Ada程序模型檢測研究.pdf

1、隨著多核處理器的發(fā)展，Ada并發(fā)程序已經(jīng)普遍應(yīng)用于現(xiàn)代嵌入式軟件系統(tǒng)設(shè)計中，如何保證其正確性和可靠性成為一個十分重要的問題。模型檢測驗證并發(fā)程序已成為一種趨勢，其關(guān)鍵問題是建模，通常采用手工方式，但是這種方式存在成本高、易引入模型錯誤等缺點。同時，模型檢測還面臨一個狀態(tài)爆炸問題。因此，本文的主要研究工作著眼于利用程序切片技術(shù)減少狀態(tài)，以及Ada程序的模型提取技術(shù)，實現(xiàn)使用模型檢測工具SPIN自動檢測Ada程序。
　　針對模型提取技

2、術(shù)，本文設(shè)計了一套對Ada程序提取PROMELA模型的方法，較好地處理了大部分Ada語言特性，比如創(chuàng)建類型和子類型、并發(fā)任務(wù)機制等。同時，實現(xiàn)了一個自動化模型提取工具AdaToSpin，分為詞法分析、語法分析的分析模塊和Ada到PROMELA的轉(zhuǎn)換模塊。
　　針對狀態(tài)爆炸問題，本文提出了一種基于LTL性質(zhì)的Ada并發(fā)程序切片方法。分為三步：首先，分析程序中語句間的各種依賴關(guān)系，構(gòu)造Ada程序的并發(fā)程序依賴圖；其次，根據(jù)系統(tǒng)待驗證的