現在，計算機和軟件比以往任何時候都更加重要。在汽車、飛機和醫療設備等系統中，執行沒有重大缺陷或“故障”（bug）的軟件非常重要。據外媒報道，荷蘭埃因霍溫理工大學（Eindhoven University of Technology）在讀博士生Thomas Neele基于模型檢查法研發了三種技術，以更智能、更快速地檢查軟件故障。

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

Neele研發的三項技術有一個共同點：會考慮到軟件系統狀態的要求，這條額外的信息使其更容易了解到哪部分不需要檢查。為了能夠同時觀察系統的行為和要求，Neele首先新研發了一種結構化的方法，以展示行為與要求相結合的信息。

第一項技術通過將相似的狀態組在一起減少了所需要檢查的狀態的數量，甚至可以處理無窮數量的狀態。第二項技術可以檢查可以并行工作的軟件部分是否有時在獨立執行任務。在此種情況下，沒有必要檢查所有可能的狀態。最后一種技術可以檢查某些元素是否有相關性，如果不相關則將其刪除。

未來，上述想法將有助于減少研發成本，縮短安全關鍵軟件的上市時間，讓高科技醫療服務更便宜，從而讓更多人可以享受此種服務。此外，Neele的技術還可以幫助從飛機、汽車等系統中清除危險的故障。目前，應用Neele的想法和模型檢查法需要大量的專業知識。為了讓其技術得以大規模采用，有必要研發一種全自動化系統，以決定哪種方法最適用于某一特定應用。
責任編輯：YYX