Analyzing and Debugging Normative Requirements via Satisfiability Checking
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929206621896704 |
|---|---|
| author | Feng, Nick Marsso, Lina Yaman, Sinem Getir Baatartogtokh, Yesugen Ayad, Reem de Mello, Victória Oldemburgo Townsend, Beverley Standen, Isobel Stefanakos, Ioannis Imrie, Calum Rodrigues, Genaína Nunes Cavalcanti, Ana Calinescu, Radu Chechik, Marsha |
| author_facet | Feng, Nick Marsso, Lina Yaman, Sinem Getir Baatartogtokh, Yesugen Ayad, Reem de Mello, Victória Oldemburgo Townsend, Beverley Standen, Isobel Stefanakos, Ioannis Imrie, Calum Rodrigues, Genaína Nunes Cavalcanti, Ana Calinescu, Radu Chechik, Marsha |
| contents | 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 challenge, 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 (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which 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 ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_05673 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Analyzing and Debugging Normative Requirements via Satisfiability Checking Feng, Nick Marsso, Lina Yaman, Sinem Getir Baatartogtokh, Yesugen Ayad, Reem de Mello, Victória Oldemburgo Townsend, Beverley Standen, Isobel Stefanakos, Ioannis Imrie, Calum Rodrigues, Genaína Nunes Cavalcanti, Ana Calinescu, Radu Chechik, Marsha Software Engineering 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 challenge, 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 (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which 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 ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots. |
| title | Analyzing and Debugging Normative Requirements via Satisfiability Checking |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2401.05673 |