Introduction

People

Papers

Screenshots

System requirements

Download

Installation

Bugs

Reserved area

Introduction

Tropos is an agent-oriented software development methodology founded on two novel features. First, the methodology is defined in terms of the concepts of agent, goal, and related mentalistic notions. These notions are used to support all software development phases, from early requirements analysis to implementation. Second, a crucial role is given to early requirements analysis that precedes prescriptive requirements specification for the system-to-be. As such, Tropos supports earlier phases of software development compared to other agent- and object-oriented methodologies.
Software development begins by identifying relevant stakeholders (represented as actors) and their goals. These root goals are analyzed, refined, and delegated to existing on new actors. The system-to-be and its components come about as new actors who are responsible for the fulfillment of some of the original or refined goals. The whole process ends when sufficient goals have been delegated so that if all actors fulfill their responsibilities, all root goals are fulfilled. Goal analysis process is made concrete by using a formal goal model model. This goal model supports both qualitative and quantitative relationships between goals, and can be used to perform two types of analysis. The first type (forward reasoning) answers questions of the form: Given a goal model, and assuming that certain leaf goals are fulfilled, are all root goals fulfilled as well? The second type of analysis (backward reasoning) solves problems of the form: Given a goal model, find a set of leaf goals that together fulfill all root goals.

Forward reasoning. Given a goal graph and an initial values assignment to some goals, input goals from now on (typically leaf goals), forward reasoning focuses on the forward propagation of these initial values to all other goals of the graph according to the rules described in Section 3. Initial values represent the evidence available about the satisfaction and the denial of a specific goal, namely evidence about the state of the goal. Usually such a evidence corresponds to qualitative values of satisfaction or denial of a goal. This is mainly because the evidence is usually provided very vaguely by the stakeholders, during the interviews with the analyst, or elaborated from documents or other available sources of information.
For each goal we consider three values representing the current evidence of satisfi- ability and deniability of goal: F (full), P (partial), N (none).We admit also conflicting situations in which we have both evidence for satisfaction and denial of a goal. So for instance, we may have that for goal G we have fully (F) evidence for the satisfaction and at the same time partial (P) evidence for denial. This could represent a situation in which we have two difference sources of information that provide conflicting evidence, or a multiple decompositions of goal G, where some decompositions suggest satisfaction of G while others suggest denial.
After the forward propagation of the initial values, the user can look the final values of the goals of interest, target goals from now on (typically root goals), and reveal possible conflicts. In other words, the user observes the effects of the initial values over the goals of interests.

Backward reasoning. Backword reasoning focuses on the backward search of the possible input values leading to some desired final value, under desired constraints. We set the desired final values of the target goals, and we want to find possible initial assignments to the input goals which would cause the desired final values of the target goals by forward propagation. We may also add some desired constraints, and decide to avoid strong/medium/weak conflicts.
Figure 1
So for instance, in the goal model of Figure 1 we may be interested in finding an assignment without any conflict such that the top goal manage internet shop and the softgoal security are both fully satisfied. Our solution reduces the problem of the backward reasoning to that of propositional satisfiability (SAT).

The GR-Tool. Forward and backward reasoning is supported in Tropos by a Goal Reasoning Tool (GR-Tool). Basically, the GR-Tool is graphical tool in which it is possible to draw the goal models and run the algorithms and tools for forward and backward reasoning. The algorithms for the forward reasoning have been fully developed in java and are embedded in the GR-Tool.
For the backward reasoning we have implemented a tool called GOALSOLVE. The schema of GOALSOLVE is reported in Figure2 (black arrows).
Figure 2
GOALSOLVE takes as input a representation the goal graph, a list of desired final values and, optionally, a list of user desiderata and constraint and a list of goals which have to be considered as input. The user may also activate some flags for switching on the various levels of ``avoiding conflicts''.
The first component of GOALSOLVE is an encoder that generates a boolean CNF formula Phi plus a correspondence table between goal values and their correspondent boolean variable. Phi is given as input to the SAT solver CHAFF, which returns either ``UNSAT'' if Phi is unsatisfiable, or ``SAT'' plus a satisfying assignment mu if Phi is satisfiable. Then a decoder uses the table to decode back the resulting assignment into the set of goal values.
In order to deal the minimum cost solutions, we have implemented a variant of GOALSOLVE, called GOALMINSOLVE, for the search of the goal values of minimum cost. The schema of GOALSOLVE is reported in Figure2 (gray arrows). Unlike GOALSOLVE, GOALMINSOLVE takes as input also a list of integer weights W(val(G)) for the goal values, with some default options. The encoder here encodes also the input weight list into a list of weights for the corresponding boolean variables of Phi. Both Phi and the list of weights are given as input to the minimum-weight SAT solver MINWEIGHT, which returns either ``UNSAT'' if Phi is unsatisfiable, or ``SAT' plus a minimum-weight satisfying assignment mu if Phi is satisfiable. The decoder then works as in GOALSOLVE.


People

Paolo Giorgini - University of Trento, Italy
John Mylopoulos - University of Toronto, Canada
Roberto Sebastiani - University of Trento, Italy
Alberto Siena - University of Trento, Italy

Papers

R. Sebastiani, P.Giorgini, and J. Mylopoulos. Simple and Minimum-Cost Satisfiabilityfor Goal Models. In Proceedings of the 16th Conference On AdvancedInformation Systems Engineering (CAiSE*04), LNCS Springer, 2004.

P. Giorgini, E. Nicchiarelli, J. Mylopoulous, R. Sebastiani. FormalReasoning Techniques for Goal Models. Journal of Data Semantics.Springer, LNCS 2800 - Journal Subline, 2004.

P. Giorgini, J. Mylopoulos, E. Nicchiarelli and R. Sebastiani.Reasoningwith Goal Models. Proceedings ofthe 21st International Conference on conceptual Modeling (ER2002),Tampere, Finland, October 2002. LNCS - Springer Verlag.

Screenshots

Some screenshots of the tool can be found here

System requirements


Download

GR-Tool package is no longer available for download, as it has been superseded by CGM-Tool; please follow the link to download a copy.

Installation

Once the jvm is correctly installed, you just need to unpack the downloaded file into a directory.

To run it, double-click the GoalEditor.jar file, or type at the shell:

java -jar GoalEditor.jar

Note: if you want to launch the solvers under unix or mac, the solver directory must be fully readable and writable, and te solvers must also be executable:
chmod -R ugo+rwx solver

Bugs

Please submit any bug report to CGM-Tool support staff.


Note for Unix, Linux and MacOS X:

Paolo Giorgini