Formal analysis of early requirements specifications
Ariel Fuxman · Library and Archives Canada (Government of Canada) · 2001
Early Requirements Engineering is the phase of the software development process that is concerned with understanding the organizational context of a system, and the goals and social dependencies of its stakeholders. Formal Methods techniques have a great potential as a powerful means for specification, early debugging and certification of software. So far, however, their application to early requirements modeling and analysis has been limited by a mismatch between the concepts used for describing early requirements and the constructs offered by formal specification languages. This thesis describes an approach that bridges the gap between Early Requirements Engineering and Formal Methods. In particular, we propose a new specification language, called Formal Tropos, that offers the primitive concepts of early requirements frameworks (actor, goal, strategic dependency), and supplements them with a rich temporal specification language. We also developed a tool, called T-Tool, that is able to perform formal analysis on the Formal Tropos specifications. The tool is based on Formal Methods techniques, in particular model checking. Our preliminary experiments on a case study show that formal analysis techniques reveal gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis tools.