|
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
ft@dit.unitn.it. Please contact ft@dit.unitn.it if you need
assistance in the download, in the compilation or in the usage of the T-Tool.
|
||||||