Hugo

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.

Specification of state machines

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.

Distribution

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.

Installation

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/.

Execution

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:

Options

Help (-?)

Shows a brief description of Hugo's usage.

Collaborations (-c file)

Hugo check, whether a particular collaboration is possible for the given set of state machines. A collaboration is provided by the run time option -c followed by the name of a text file. This text file specifies the collaboration and consists of two parts:

The declaration of the instances used in the collaboration (each on a separate line),
The collaboration's interaction that should be verified (separated by semicolons). If you specify several interactions, Hugo will check if one of those interactions is possible.

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.

Orthogonal regions (-f)

As the order in which orthogonal regions handle an event is unspecified by the UML, all possible orderings are checked. This non-determinism is irrelevant for most models but carries a hefty performance penalty during verification. The option -f allows to restrict verification to a fixed ordering of orthogonal regions.

Only make send events available after RTC step (-s)

Usually send events are immediately available to other state machines, even if the sending state machine has not yet completed its run-to-completion step. As this behavior is irrelevant for most models, this option can be used to decrease the verification complexity.

Size of event queues (-q N)

This option sets the size of the event queues to N. Default is 4.

Only generate Promela code (-p)

With this option Hugo will only generate Promela code and not start the verification runs.

Additional information

We tested Hugo with XMI files of UML models that were made with the free CASE-tool Argo/UML v0.8.1a (http://argouml.tigris.org/). Note that Argo/UML sometimes writes errors into the XMI-file. This may result in an exception message that can be ignored.
Most CASE-tools do not support concurrent composite states. As a workaround we consider a composite state that contains the text '(concurrent)' in its name a concurrent composite state. All its substates (that need to be non-concurrent composite states) are considered the orthogonal regions.
If your CASE-tool doesn't support the specification of do-activities, you may start an entry-action with 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.
If you do not have a document type definition file for XML 1.3 (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.

Restrictions

Hugo can only check state machines that are syntactically correct, according to the OMG Unfied Modeling Language Specification, Version 1.3. Hugo may abort upon a syntactical incorrectness, yet it does not recognise all syntax errors.
A transition out of an initial state needs to target a non-pseudostate and may not have a guard.
The default transition out of a history state may not target another history state or a junction pseudostate. It may not have a guard.
The use of multiple instances of one class is currently not supported.

Currently unsupported UML constructs:

internal transitions
event parameters
signal hierarchies
deferred events
synch states
choice states
change events
time events

This product includes software developed by the Apache Software Foundation (http://www.apache.org/).