为了确保信息物理系统(CPS)和物联网系统的安全，我们需要识别对手如何利用现有原子漏洞之间的相互依赖性来组织可能危及系统的攻击。因此，在系统安全中，生成准确的攻击图十分重要。

基于手动构建攻击图繁琐且容易出错的原因，Alaa T. Al Ghazo等人2019年5月在《IEEE系统：人和控制论会刊》发表文章，提出了一种基于模型检验的自动攻击图生成器和可视化工具(A2G2V)。A2G2V算法使用现有的模型检验工具、架构描述工具和自编代码来生成攻击图，该攻击图列举了原子级漏洞可能被利用来危及系统安全的所有可能序列集。

架构描述工具给出了网络系统、其原子漏洞和前后条件以及相关安全属性的形式化表达。模型检测器自动识别表现为反例形式的攻击序列。自编代码与模型检测器集成在一起，解析反例，放宽规范对反例进行编码，并迭代直到揭示所有攻击序列。最后，A2G2V还集成了可视化工具，用图形展示已生成的攻击图。实验结果在计算机和控制(SCADA)网络中的应用得到了验证。