Tool for Supporting Debugging and Understanding of Normative Requirements Using LLMs

TL;DR

This paper presents SLEEC-LLM, a tool leveraging large language models to interpret formal verification counterexamples in natural language, thereby aiding non-technical stakeholders in understanding and validating normative requirements efficiently.

Contribution

The paper introduces SLEEC-LLM, a novel tool that enhances normative requirements analysis by translating formal verification results into accessible natural language explanations using LLMs.

Findings

Improves understanding of formal verification results for non-technical users.

Reduces time and effort in requirements validation process.

Effective in real-world case studies with diverse stakeholders.

Abstract

Normative requirements specify social, legal, ethical, empathetic, and cultural (SLEEC) norms that must be observed by a system. To support the identification of SLEEC requirements, numerous standards and regulations have been developed. These requirements are typically defined by stakeholders in the non-technical system with diverse expertise (e.g., ethicists, lawyers, social scientists). Hence, ensuring their consistency and managing the requirement elicitation process are complex and error-prone tasks. Recent research has addressed this challenge using domain-specific languages to specify normative requirements as rules, whose consistency can then be analyzed with formal methods. Nevertheless, these approaches often present the results from formal verification tools in a way that is inaccessible to non-technical users. This hinders understanding and makes the iterative process of eliciting and validating these requirements inefficient in terms of both time and effort. To address this problem, we introduce SLEEC-LLM, a tool that uses large language models (LLMs) to provide natural-language interpretations for model-checking counterexamples corresponding to SLEEC rule inconsistencies. SLEEC-LLM improves the efficiency and explainability of normative requirements elicitation and consistency analysis. To demonstrate its effectiveness, we summarise its use in two real-world case studies involving non-technical stakeholders.