通过可满足性检查分析与调试规范性需求
软件工程
2024-01-12 v1
摘要
随着软件系统在交通和医疗等应用领域与人类的交互日益增多，它们引发了与利益相关者的社会、法律、伦理、共情和文化（SLEEC）规范和价值观相关的担忧。规范性非功能需求（N-NFRs）用于通过设定与 SLEEC 相关的系统行为边界来捕获这些担忧。由于 N-NFRs 需要由具有广泛不同非技术专长的多个利益相关者（伦理学家、律师、监管者、最终用户等）来指定，N-NFR 的获取非常具有挑战性。为应对这一挑战，我们引入了 N-Check，这是一种新颖的工具支持的、用于 N-NFR 分析和调试的形式化方法。N-Check 采用可满足性检查来识别广泛的 N-NFR 合式性问题（WFI），例如冲突、冗余、限制性、不足，并生成诊断信息，以用户友好的方式精确定位其原因，使非技术利益相关者能够理解并修复它们。我们通过九个案例研究展示了我们方法的有效性和可用性，在这些案例中，由伦理学家、律师、哲学家、心理学家、安全分析师和工程师组成的团队使用 N-Check 分析和调试了 233 条 N-NFRs，其中包含 62 个问题，这些 N-NFRs 支撑着从辅助护理机器人和树木病害检测无人机到制造协作机器人等系统的运行软件。
引用
@article{arxiv.2401.05673,
title = {Analyzing and Debugging Normative Requirements via Satisfiability Checking},
author = {Nick Feng and Lina Marsso and Sinem Getir Yaman and Yesugen Baatartogtokh and Reem Ayad and Victória Oldemburgo de Mello and Beverley Townsend and Isobel Standen and Ioannis Stefanakos and Calum Imrie and Genaína Nunes Rodrigues and Ana Cavalcanti and Radu Calinescu and Marsha Chechik},
journal= {arXiv preprint arXiv:2401.05673},
year = {2024}
}