| 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. |
