現(xiàn)在，計(jì)算機(jī)和軟件比以往任何時(shí)候都更加重要。在汽車(chē)、飛機(jī)和醫(yī)療設(shè)備等系統(tǒng)中，執(zhí)行沒(méi)有重大缺陷或“故障”（bug）的軟件非常重要。據(jù)外媒報(bào)道，荷蘭埃因霍溫理工大學(xué)（Eindhoven University of Technology）在讀博士生Thomas Neele基于模型檢查法研發(fā)了三種技術(shù)，以更智能、更快速地檢查軟件故障。

模型檢查是最嚴(yán)格的軟件檢查技術(shù)之一，可以檢查一個(gè)軟件系統(tǒng)所能完成的所有事情，其能夠處于的“狀態(tài)”以及檢查是否其能夠按要求工作。軟件常常由許多可以并行工作的部分組成，這可能導(dǎo)致需要檢查的部分的數(shù)量激增，導(dǎo)致檢查模型成本高昂，甚至可能最終導(dǎo)致無(wú)法進(jìn)行管理。Neele探索了新方法，通過(guò)減少需要檢查的部分的數(shù)量，以解決該問(wèn)題。

Neele研發(fā)的三項(xiàng)技術(shù)有一個(gè)共同點(diǎn)：會(huì)考慮到軟件系統(tǒng)狀態(tài)的要求，這條額外的信息使其更容易了解到哪部分不需要檢查。為了能夠同時(shí)觀察系統(tǒng)的行為和要求，Neele首先新研發(fā)了一種結(jié)構(gòu)化的方法，以展示行為與要求相結(jié)合的信息。

第一項(xiàng)技術(shù)通過(guò)將相似的狀態(tài)組在一起減少了所需要檢查的狀態(tài)的數(shù)量，甚至可以處理無(wú)窮數(shù)量的狀態(tài)。第二項(xiàng)技術(shù)可以檢查可以并行工作的軟件部分是否有時(shí)在獨(dú)立執(zhí)行任務(wù)。在此種情況下，沒(méi)有必要檢查所有可能的狀態(tài)。最后一種技術(shù)可以檢查某些元素是否有相關(guān)性，如果不相關(guān)則將其刪除。

未來(lái)，上述想法將有助于減少研發(fā)成本，縮短安全關(guān)鍵軟件的上市時(shí)間，讓高科技醫(yī)療服務(wù)更便宜，從而讓更多人可以享受此種服務(wù)。此外，Neele的技術(shù)還可以幫助從飛機(jī)、汽車(chē)等系統(tǒng)中清除危險(xiǎn)的故障。目前，應(yīng)用Neele的想法和模型檢查法需要大量的專(zhuān)業(yè)知識(shí)。為了讓其技術(shù)得以大規(guī)模采用，有必要研發(fā)一種全自動(dòng)化系統(tǒng)，以決定哪種方法最適用于某一特定應(yīng)用。
責(zé)任編輯：YYX