基于有界可满足性检查的法规合规性早期验证
软件工程
2023-05-30 v3
摘要
法律属性涉及对数据值和时间推理。度量一阶时序逻辑（MFOTL）为规约法律属性提供了丰富的 formalism。尽管 MFOTL 已通过运行时监控成功用于运营系统的法律属性验证，但对于以需求捕获的早期系统开发中基于 MFOTL 的验证尚不存在解决方案。给定一个以 MFOTL 形式化的法律属性和系统需求，可通过可满足性检查在需求上验证该属性的合规性。本文提出一种实用、可靠且完全（在给定边界内）的 MFOTL 可满足性检查方法。该方法基于可满足性模理论（SMT），采用反例引导策略增量搜索满足解。我们使用 Z3 SMT 求解器实现了该方法，并在涵盖医疗、行政管理、银行和航空领域的五个案例研究上进行了评估。结果表明，我们的方法能有效判定关注的法律属性是否满足，或生成导致合规违规的反例。
引用
@article{arxiv.2209.04052,
title = {Early Verification of Legal Compliance via Bounded Satisfiability Checking},
author = {Nick Feng and Lina Marsso and Mehrdad Sabetzadeh and Marsha Chechik},
journal= {arXiv preprint arXiv:2209.04052},
year = {2023}
}