使用目标导向的答案集编程自动化系统保证案例的语义分析
计算机科学中的逻辑
2025-01-22 v5 软件工程
摘要
保证案例为论证和证据提供了一种结构化方式，用于对安全性和保密性至关重要的系统进行认证。然而，创建和评估这些保证案例可能复杂且具有挑战性，即使对于中等复杂度的系统也是如此。因此，越来越需要为这些任务开发新的自动化方法。虽然大多数现有的保证案例工具侧重于自动化结构方面，但它们缺乏全面评估保证论证的语义一致性和正确性的能力。在先前的工作中，我们引入了Assurance 2.0框架，该框架优先考虑推理过程、证据利用以及反主张（击败者）和反证据的明确界定。在本文中，我们介绍了使用常识推理和答案集编程求解器（特别是s(CASP)）来增强Assurance 2.0的语义规则分析能力的方法。通过采用这些分析技术，我们检查了保证案例的独特语义方面，例如逻辑一致性、充分性、不可击败性等。这些分析的应用为系统开发人员和评估人员提供了对保证案例的更高信心。
引用
@article{arxiv.2408.11699,
title = {Automating Semantic Analysis of System Assurance Cases using Goal-directed ASP},
author = {Anitha Murugesan and Isaac Wong and Joaquín Arias and Robert Stroud and Srivatsan Varadarajan and Elmer Salazar and Gopal Gupta and Robin Bloomfield and John Rushby},
journal= {arXiv preprint arXiv:2408.11699},
year = {2025}
}