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

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

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