ST-Tool

General Information

Tool Name

ST-Tool (Secure Tropos)

Version

v. 1.4

Group

University of Trento

Web page (if available)

http://sesa.dit.unitn.it/sttool/index.php

Main Purpose of the Tool

ST-Tool, the Secure Tropos tool, is a graphical CASE tool where it is possible to draw Tropos and Secure Tropos models and to perform the effective formal analysis of functional and security requirements. The tool is written in Java with the swing components, and uses XML as its document format. Formal analysis is based on logic programming. ST-Tool provides direct support for completing and checking models expressed in Datalog specification by using different external ASP solvers, namely ASSAT, Cmodels, Smodels, and the DLV system.

i* framework supported

Tropos, Secure Tropos

Availability of the tool

• ( ) For i* modelling only
• ( ) For development only
• (X) Both

Programming Language

Java, Datalog

Platform Requirements

The Java Runtime Environment (j2sdk1.4.1_02) or above

Other technology needed

In order to perform datalog analysis, you also need a Datalog solver. ST-Tool supports 5 Datalog solvers:
ASSAT (supported only on Linux)
Cmodels-1 (supported only on Linux)
Cmodels-2 (supported only on Linux)
DLV
Smodels (supported only on Linux)

Current state of the tool

Ongoing work

i* Modelling Suitability

1. Does the tool allow SD modelling?

Yes

2. Does the tool allow SR modelling?

Yes

3. Does the tool allow working with SD & SR models jointly?

ST-tool support the modeling of SD & SR models jointly by means of expandable elements.

4. Does the tool allow the construction of the models graphically?

ST-tool allows designers to visually insert, edit or remove graphical objects in graphical layer by selecting from the top menu the desired entity or relation.

5. Does the tool allow the construction of the models textually?

ST-tool allows designers to edit the model in the form of Datalog specification.

6. Describe how the elements are modelled and their flexibility (i.e., the elements can be moved and reordered).

7. Describe how the dependency links are modelled and their flexibility (i.e., dependencies are modelled with straight lines that can not be redirected).

8. Does the tool allow automatic organization of the elements?

Yes / No

9. Other modelling facilities provided by the tool:

• ST-Tool supports two types of collapsing nodes, namely collapsing services and actors. When a service is collapsed, its sub-services, decomposition arcs and relations having subservices as dependum are hidden. When an actor is collapsed, the entire goal diagram of the actor is hidden.
• ST-tool also allows designers to activate one or more views of the requirements model (i.e. dependency diagram for Tropos, and trust diagram, functional requirements diagram and trust management implementation for Secure Tropos) at the same time. Essentially, when a view is deactivated, all elements related to that particular view are hidden.

10. Does the tool check SD models?

ST-tool analyzes the graphical requirements model and reports errors such as "isolated nodes" (i.e. goals, tasks, or resources not involved in any relation), "orphan relations" (i.e. relations where an arc is missing), and bad-typed relations.

11. Does the tool check SR models?

ST-tool analyzes the graphical requirements model and reports errors such as "isolated nodes" (i.e. goals, tasks, or resources not involved in any relation), "orphan relations" (i.e. relations where an arc is missing), and bad-typed relations.

12. Other checks provided by the tool (i.e., cross validation between SD and SR models).

• Although visual modeling has been recognized as a fundamental feature of the software development process so that designers and stakeholders can understand each other, graphical models are not suitable for formal requirements analysis. Moreover, the extensional description of the system cannot be directly used for requirements verification. Actually, the model drawn during the modeling phase fails to answer stakeholder questions like ``Who is actually authorized to access my own resources?, ``Are my objectives fulfilled?, etc. These issues have motivated the introduction of a formal framework supporting the Secure Tropos methodology. Essentially, the formal framework defines the semantics used to complete and verify the rcorrectness and consistency of the equirements model

13. Does the tool allow working with two or more models at the same time?

No

14. Does the tool allow to group models in projects?

No

15. Does the tool allow working with two or more projects at the same time?

No

16. What are the other functionalities that the tool provides?

In order to verify consistency and correctness of system requirements, ST-Tool supports the automatic transformation of graphical models into formal specifications. Currently, two logics are supported: temporal logic for behavioral specification and answer set programming for security verification.

Usability

17. Rate the understandability of the user interface

• ( ) Internal use
• ( ) Ready for public use
• (X) Has been used publicly

18. Rate the quality of the user manual

• ( ) Inexistent
• ( ) Internal use
• ( ) Ready for public use
• (X) Has been used publicly

19. Does the tool provides i* learning facilities?

No

20. Does the tool provide any examples for the users?

Yes

21. Rate the difficulty of installing the tool

• ( ) Copy files and initializing paths
• (X) Copy files
• ( ) Executable installation file provided

Maturity of the Tool

22. Rate the maturity of the tool from the user point of view:

• ( ) Under Development
• (X) Prototype
• ( ) Ready for public use
• ( ) Has been used publicly

If not for public use, mark one or more of the following:

• ( ) incomplete
• ( ) occasional testing
• (X) non-exhaustive testing
• ( ) non-persistent data
• ( ) poor efficiency
• ( ) not portable
• ( ) others: please specify

Expected date for public use (if any):

23. Has the tool been used for any case study?

• The Compliance with the Italian Data Protection Legislation by the University of Trento
• John Rusnak and the Allied Irish Bank

24. Has the tool been tested in large models?

Yes

25. Has the tool any drawback when working with very large models?

No

26. Which is approximately the maximum size of the model (in terms of actors and dependencies) the tool has been used for?

The analysis of requirements models involving more than 100 actors require more or less 5 sec. We have not tried with bigger models, but we believe that the tool can deal with them in a reasonable time.

Extensibility and Interoperability

27. Does the tool allow importing files?

The tool support the importing of Datalog files.

28. Does the tool allow exporting files?

Yes
XML, Formal Tropos, Datalog, pictures of the graphical representatio

29. Does the tool allow importing/exporting the data through an XML format?

Yes / No
If so, link to the DTD for the XML format if available.

30. Is the architecture of the tool published?

Yes / No
If so, where?

31. Does the tool allow the addition of other elements outside the i* framework of the tool?

Yes / No

32. New functionalities can be added to the tool by means of:

• ( ) PLUG-IN
• ( ) Open-Source code
• ( ) import & export XML
• ( ) NONE

33. Rate the maturity of the tool from for open development:

• ( ) Under Development
• (X ) Prototype
• ( ) Ready for public development use
• ( ) Has been used for public development

If not for public development use, mark one or more of the following:

• ( ) incomplete code
• (X) no help provided
• ( ) non-persistent data
• ( ) non-exhaustive testing
• ( ) poor efficiency
• ( ) not portable
• ( ) no development installation facilities provided
• ( ) others: please specify

Expected date for public development use (if any):

34. Is there any internal documentation for programmers?

No