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

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

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