計算機和軟件比以往任何時候都重要。在汽車，飛機和醫(yī)療設(shè)備等系統(tǒng)中，實現(xiàn)無重大缺陷或“錯誤”的軟件至關(guān)重要。埃因霍溫科技大學(xué)博士學(xué)位 候選人Thomas Neele基于模型檢查方法開發(fā)了三種技術(shù)，可以更智能，更快速地進行錯誤檢查。

模型檢查是檢查軟件的最嚴格的技術(shù)之一。它檢查軟件系統(tǒng)可以做的所有可能的事情，以及可以進入的“狀態(tài)”，以檢查其是否按要求工作。挑戰(zhàn)在于軟件通常由許多并行工作的部分組成。這可能會導(dǎo)致需要研究的狀態(tài)數(shù)量激增，使模型檢查成本高昂，甚至難以管理。Neele探索了通過減少需要檢查的狀態(tài)數(shù)來解決此問題的新方法。

牢記軟件目標

Neele開發(fā)的三種新的還原技術(shù)有一個共同點：它們牢記狀態(tài)的要求。這些額外的信息意味著更容易查看哪些狀態(tài)不需要檢查。為了能夠同時查看系統(tǒng)的行為和要求，Neele首先開發(fā)了一種新的結(jié)構(gòu)化方法來顯示行為與需求的組合。

第一種技術(shù)是通過將相似狀態(tài)分組在一起來減少狀態(tài)數(shù)量。這樣甚至可以處理無數(shù)個狀態(tài)。第二種方法檢查并行工作的部分是否有時獨立執(zhí)行任務(wù)。在這種情況下，不必研究所有可能的狀態(tài)。最后一種技術(shù)是檢查某些數(shù)據(jù)元素是否相關(guān)，如果不相關(guān)則將其刪除。

使軟件更安全，更快

將來，這些想法將有助于降低安全關(guān)鍵軟件的開發(fā)成本和上市時間。這可以使高科技醫(yī)療保健更加實惠，從而使每個人都可以使用。此外，Neele的技術(shù)可以幫助消除飛機等系統(tǒng)中的危險錯誤。當前，Neele的思想的應(yīng)用以及一般的模型檢查需要大量的專業(yè)知識。為了能夠被廣泛采用，有必要開發(fā)一個全自動系統(tǒng)來決定哪種方法最適合特定應(yīng)用。