Formal Tropos aims to an effective integration and harmonization of Formal Methods in the Tropos Software Development Process.

Formal Tropos provides a specification language that offers the primitive concepts of early requirements specification of i* (actor, goal, strategic dependency), but supplements them with a rich temporal specification language inspired by the KAOS project.

The i* notation allow for the description of the ``structural'' aspects of the early requirements model, for instance in terms of the network of relationships and dependencies among actors. Formal Tropos permits to represent also the ``dynamic'' aspects of the model, describing for instance how the network of relationships evolves over time. In Formal Tropos one can define the circumstances under which a given dependency among two actors arises, as well as the conditions that permit to consider the dependency fulfilled.

The representation and the analysis of these dynamic aspects allows for a more precise understanding of the early requirements model, and reveals gaps and inconsistencies that are by no means trivial to discover without the help of formal analysis tools.

In order to support the automated analysis of Formal Tropo specifications, we have extended an existing formal verification technique, model checking.

We have also implemented this extension in a tool, called the T-Tool, which is based on the state-of-the-art symbolic model checker NuSMV.

The T-Tool translates automatically an Formal Tropos specification into an Intermediate Language specification that could potentially link Formal Tropos with different verification engines.

The Intermediate Language representation is then automatically translated into NuSMV, which can then perform different kinds of formal analysis, such as consistency checking, animation of the specification, and property verification.

Reports on the effectiveness of the Formal Tropos approach can be found here