一句话：提出 N-Check，用可满足性检查自动发现并诊断规范性非功能需求中的冲突、冗余、过强限制与不足等问题。
随着软件在交通、医疗等领域与人类交互增多，需捕获社会、法律、伦理、共情与文化（SLEEC）规范。规范性非功能需求（N-NFR）为系统行为设定这些边界，但需由伦理学家、律师、监管者、用户等非技术利益相关者共同提出，分析与调试困难。论文提出 N-Check：一种工具支持的形式化方法，利用可满足性检查识别 N-NFR 的冲突、冗余、过强限制和不足等良构性问题，并生成用户友好诊断以定位原因、帮助非技术用户理解并修复。九个案例研究中，伦理学家、律师、哲学家、心理学家、安全分析师和工程师使用 N-Check 分析了 233 条 N-NFR，涉及辅助护理机器人、树木病害检测无人机和制造业协作机器人，共发现 62 个问题，表明其有效性与可用性。
As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this difficult task, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues, such as conflicts, redundancy, restrictiveness, and insufficiency, yielding diagnostics that pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs, comprising 62 issues for the software underpinning the operation of systems, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
DOI 原文 ·
@inproceedings{paperbot11471,
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 Victoria Oldemburgo De Mello and Beverley Townsend and Isobel Standen and Ioannis Stefanakos and Calum Imrie and Genaina Nunes Rodrigues and Ana Cavalcanti and Radu Calinescu and Marsha Chechik},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3639093}
}