為了確保信息物理系統(tǒng)(CPS)和物聯(lián)網(wǎng)系統(tǒng)的安全，我們需要識別對手如何利用現(xiàn)有原子漏洞之間的相互依賴性來組織可能危及系統(tǒng)的攻擊。因此，在系統(tǒng)安全中，生成準確的攻擊圖十分重要。

基于手動構建攻擊圖繁瑣且容易出錯的原因，Alaa T. Al Ghazo等人2019年5月在《IEEE系統(tǒng)：人和控制論會刊》發(fā)表文章，提出了一種基于模型檢驗的自動攻擊圖生成器和可視化工具(A2G2V)。A2G2V算法使用現(xiàn)有的模型檢驗工具、架構描述工具和自編代碼來生成攻擊圖，該攻擊圖列舉了原子級漏洞可能被利用來危及系統(tǒng)安全的所有可能序列集。

架構描述工具給出了網(wǎng)絡系統(tǒng)、其原子漏洞和前后條件以及相關安全屬性的形式化表達。模型檢測器自動識別表現(xiàn)為反例形式的攻擊序列。自編代碼與模型檢測器集成在一起，解析反例，放寬規(guī)范對反例進行編碼，并迭代直到揭示所有攻擊序列。最后，A2G2V還集成了可視化工具，用圖形展示已生成的攻擊圖。實驗結果在計算機和控制(SCADA)網(wǎng)絡中的應用得到了驗證。