Current version is 2.00 (updated on the 28th of June, 2001).
See the list of changes here. Please reread this page for the usage of new features.
The state machines that should be verified need to be specified for classes in a UML-model, which is exported into a XMI-file (version 1.3). These classes need to be in one and the same package. If the given set of state machines send messages to each other, their classes need to be connected by an association, whose role names are used to refer to the targeted state machine. Moreover, each class should only have one state machine. Each class needs to declare the call and send events that it can receive: call event reception is declared by a public method with the same name as the event, e.g. public void e()
; send event reception is declared by a method receive
with the accepted signal as parameter, e.g. public void receive(Signal s)
.
Actions may emit send or call events (e.g. ^e'
, ^c1.s
). Actions and Guards may contain Promela code. If the Promela code should read or manipulate variables that are visible to an entire state machine, they need to be specified as attributes in the state machine's class. Multiple actions are separated by semicolons.
Do-activites need to include the command yieldDoActivity
at those points on which they allow other processes to continue executing and to give Hugo a chance to abort the do-activity before its completion. This is particularily important if you include loops in your do-activities.
The distribution includes Hugo in the archive hugo_2_00.jar
. Moreover an example model is provided, together with two collaborations and shell scripts startCollaborationCheck1
, startCollaborationCheck2
and startDeadlockCheck
. The first two have Hugo verify, whether the specific collaborations are possible between the state machines of the example model, the third one checks the state machines for deadlocks. Hugo first generates a promela model from the state machines (and collaboration). Then it has Spin generate a verifier. After that it will start the C-compiler and the verification run.
You may need to adapt the shell scripts to your system's configuration. They were tested on SuSE Linux 6.3.
The file spinExample/model/model.html
shows the example model.
Extract the distribution file hugo_2_00.tgz
.
You need a Java 1.2 (or higher) run time environment. Besides that the following libraries need to be included in the classpath:
nsuml.jar
Available at http://nsuml.sourceforge.net/. xerces.jar
Available from the xerces distribution at http://xml.apache.org/xerces-j/. The provided shell scripts expect that all archives are copied into the subdirectory lib/
.
To start Hugo run one of the shell scripts.
Hugo is always executed with the following arguments:
The name of the XMI-file that contains the model, the name of the file that the Promela code should be generated into, the name of the package the classes are in and the names of these classes.
The commands that Hugo uses to start Spin, the C-compiler and the verification run can be modified in the properties file hugo.properties
. Make sure that the classpath of the execution of Hugo includes the folder that hugo.properties
is in. If the properties file is not found, default values will be used.
The following additional options may be used behind the arguments:
-c
followed by the name of a text file. This text file specifies the collaboration and consists of two parts:
Example text file: o1:C1
o2:C2
o1^c2.e1;o2^c1.e2;o1^c2.e3
If no collaboration specification is supplied, Hugo will check for deadlocks, by finding invalid end states.
-f
allows to restrict verification to a fixed ordering of orthogonal regions.
do/
. This will have Hugo consider that entry-action a do-activity. Note that a state can't have an entry-action and a do-activity at the same time then. uml13.dtd
) in the directory in which you execute Hugo, Nsuml will warn you that it uses a default DTD. This warning can be ignored. Currently unsupported UML constructs:
This product includes software developed by the Apache Software Foundation (http://www.apache.org/).