The Formal Tropos Tool: T-Tool

T-Tool provides a framework for the effective use of formal methods in the early requirements phase. The framework allows for the formal and mechanized analysis of early requirements specifications expressed in a formal modeling language.

The specification language accepted by T-Tool is called Formal Tropos. It is a formal specification language that offers all the primitive concepts of i* (such as actors, goals, and dependencies among actors), but supplements them with a rich temporal specification language inspired by KAOS.

T-Tool allows for different kinds of analysis on a Formal Tropos specification. For instance, it allows for checking whether the specification is consistent, or whether it respects a number of desired properties. Moreover, a specification can be animated in order to give the user immediate feedback on its implications.

In order to support the mechanized analysis of Formal Tropos specifications, T-Tool applies model checking verification technique. T-Tool is built on top of NuSMV, an open-source model checker that implement state-of-the-art symbolic verification techniques.

T-Tool and Formal Tropos are part of a wider-scope framework, called Tropos, which proposes the application of concepts from the early requirements phase to the whole software development process, including late requirements, architectural and detailed design, and implementation.


T-Tool is distributed under the LGPL 2.1 licence as the NuSMV symbolic modelchecker it builds upon. The current version is the 1.0.0 version and can be downloaded in source code here. In order to use it, you have to download the NuSMV model checker as well, and the patches to the latest version of NuSMV we developed to fit the requirements of T-Tool.

For the moment, a source only version is available. Binary versions can be obtained by sending an e-mail to

Please contact if you need assistance in the download, in the compilation or in the usage of the T-Tool.

NuSMV model checker