A Domain-Specific Language for Verifying Software Requirement\n Constraints

Software requirement analysis can certainly benefit from prevention and early\ndetection of failures, in particular by some kind of automatic analysis. Formal\nmethods offer means to represent and analyze requirements with rigorous tools,\navoiding ambiguities and allowing automatic verification of requirement\nconsistency. However, formalisms often clash in the culture or lack of skills\nof software analysts, making them challenging to apply. In this article, we\npropose a Domain-Specific Language (DSL) based on Set Theory for requirement\nanalysts. The Graphical InvaRiant Language (GIRL) can be used to specify\nsoftware requirement structural invariants, with entities and their\nrelationships. Those invariants can then have their consistency evaluated by\nthe Alloy Analyzer, based on a mapping semantics we provide for transforming\nGIRL models into Alloy specifications with no user intervention. With a\nprototypical language editor and transformations implemented into an Eclipse\nplugin, we carried out a qualitative study with requirement analysts working\nfor a government software company in Brazil, to evaluate usability and\neffectiveness of the GIRL-based analysis of real software requirements. The\nparticipants were able to effectively use the underlying formal analysis, since\n79 out of 80 assigned invariants were correctly modeled. While participants\nperceived as low the complexity of learning and using GIRL's simplest,\nset-based structures and relationships, the most complex logical structures,\nsuch as quantification and implication, were challenging. Furthermore, almost\nall post-study evaluations from the participants were positive, especially as a\ntool for discovering requirement inconsistencies.\n