A Domain-Specific Language for Verifying Software Requirement Constraints

TL;DR

This paper introduces GIRL, a graphical domain-specific language based on Set Theory, designed to help requirement analysts verify software requirement invariants automatically, improving consistency detection with minimal formal skills.

Contribution

The paper presents GIRL, a new graphical DSL that simplifies formal requirement analysis and integrates with Alloy Analyzer, demonstrated through a practical Eclipse plugin and user study.

Findings

79 out of 80 invariants correctly modeled by analysts

Participants found GIRL easy for simple structures, challenging for complex logic

Positive feedback on GIRL as a tool for detecting requirement inconsistencies

Abstract

Software requirement analysis can certainly benefit from prevention and early detection of failures, in particular by some kind of automatic analysis. Formal methods offer means to represent and analyze requirements with rigorous tools, avoiding ambiguities and allowing automatic verification of requirement consistency. However, formalisms often clash in the culture or lack of skills of software analysts, making them challenging to apply. In this article, we propose a Domain-Specific Language (DSL) based on Set Theory for requirement analysts. The Graphical InvaRiant Language (GIRL) can be used to specify software requirement structural invariants, with entities and their relationships. Those invariants can then have their consistency evaluated by the Alloy Analyzer, based on a mapping semantics we provide for transforming GIRL models into Alloy specifications with no user intervention. With a prototypical language editor and transformations implemented into an Eclipse plugin, we carried out a qualitative study with requirement analysts working for a government software company in Brazil, to evaluate usability and effectiveness of the GIRL-based analysis of real software requirements. The participants were able to effectively use the underlying formal analysis, since 79 out of 80 assigned invariants were correctly modeled. While participants perceived as low the complexity of learning and using GIRL's simplest, set-based structures and relationships, the most complex logical structures, such as quantification and implication, were challenging. Furthermore, almost all post-study evaluations from the participants were positive, especially as a tool for discovering requirement inconsistencies.