Comparing Three Formal Analysis Approaches of the Tropos Family

Tropos is a software development methodology founded on concepts used to model early requirements, the i* framework. In addition to a methodological framework, research addresses also formal analysis support. In previous work, we proposed the prototype environment SNet based on the Trust-Confidence-Distrust (TCD) approach for the representation and dynamic evaluation of agent-based designs for inter-organizational networks. There are two major ingredients: i* for modeling the domain statically and ConGolog for analysing it dynamically via simulations. In this paper, we compare our approach with two other approaches that enrich i*/Tropos models to allow for more formal analyses, Formal Tropos and Secure Tropos. While the intended use of these is quite different from SNet, there are a number of commonalities, which will be highlighted as well as the differences that suggest a combined use, including complementary forms of analysis such as model checking versus simulation.