Formal Tropos
Formal Tropos is part of the Tropos project,
whose aim is to develop an agent-oriented software engineering methodology,starting from early requirements.
The methodology is to be supported by a variety of analysis tools based on formal methods. 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 |