智能的軟件錯誤怎么檢查

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

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

牢記軟件目標

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

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

使軟件更安全，更快

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