Hugo

Current version is 3.0 (updated on the 20th of November, 2002).

See the list of changes from Version 2.00 here .Please read this page for the usage of new features.

Specification of state machines

The state machines, which should be verified, need to be specified for classes in an UML-model. This model is exported into a XMI-file (version 1.3). All classes need to be in one and the same package. If a 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. Each class has to declare the call and send events, which 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). Event parameters must be added to the parameters of the method, e.g. public void e(int p1, int p2) for call events or public void receive(Signal s, int p1, int p2) for signal events (Note: all event parameters must be of the type integer).

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 must include the command yieldDoActivity at those points, on which they allow the execution of other processes. This breakpoint gives Hugo a chance to abort the do-activity before its completion. This is particularily important if you include loops in your do-activities.

Distribution

In the directory ./hugo/bin/model/ some example models are provided, together with collaborations (in ./hugo/bin/model/) and shell scripts (in ./hugo/bin/). For the example shell scripts, no additional arguments are required. Hugo first generates a Promela model from the state machines (and collaboration). Then it has Spin generate a verifier. Finally Hugo starts 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 8.0.

Installation

Extract the distribution file hugo_3_00.tgz. To compile Hugo, simply go to the ./hugo/src/ subdirectory and type 'make'.

You need a JDK 1.3.0 (or higher) to run and compile Hugo 3.00. If your Java compiler has another command then 'javac' you must modify the Makefile accordingly.

Execution

Use the run.sh shell script (in ./hugo/bin/) to start Hugo with a user defined model. If your Java interpreter has another command then 'java' you must change the file ./hugo/bin/run.sh accordingly.

Hugo is always executed with the following arguments (in exactly this order):

The name of the XMI-file that contains the model.
The name of the collaboration file.
The name of the output file, where that the Promela code should be stored.
The name of the package, which contains all classes.
The names of all used classes.

Hugo checks, whether a particular collaboration is possible for the given set of state machines. A collaboration is provided by a text file, that specifies the collaboration. It consists of three parts:

The declaration of the instances used in the collaboration (each on a separate line).
The declaration of the rolenames.
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. If the collaboration file contains no interaction specification, Hugo will check for deadlocks, by finding invalid end states.

The order of these parts must be the same as mentioned above. Lines with comments must begin with ' //'.

Example collaboration file:

     // declaration of instances:
     // format: 'instanceName:classname'
     o1:C1�� 
     o2_1:C2
     o2_2:C2

     // declaration of rolenames:
     // format: 'instanceName.rolename=associatedInstanceName'
     o1.left=o2_1
     o1.right=o2_2

     // interaction:
     // format: 'sendingInstanceName^roleName.eventName'
     o1^left.e1;o1^right.e2

The commands that Hugo uses to start Spin, the C-compiler and the verification run can be modified in the file hugo.properties. Make sure that the classpath for the execution of Hugo includes also the folder, which contains the file hugo.properties. If this file is not found, default values will be used.

The following additional options may be used after the arguments:

Options

Note: Some options from Version 2.00 have changed. See a list of changes here.

Help (-?)

Shows a brief description of Hugo's usage.

Deadlock detection (-d)

With this option you can add a deadlock detection for the model to the generated promela code. This code will automatically added, if Hugo checks for deadlocks.

Orthogonal regions (-r)

The order in which orthogonal regions handle an event is not specified by the UML. Therefor all possible orderings are checked. This non-deterministic prcedure is irrelevant for most models, but carries a performance drawback during verification. The option -r allows to restrict verification to a determined ordering of orthogonal regions.

Fire transitions in determined order (-t)

The order in which transitions are fired is not specified by the UML. So Hugo checks all possible orders during verification. If the order in which transitions are fired is irrelevant for your model you can restrict verification to a fixed order of transition firing with this option. This can result in a better performance for some models.

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. Verification runs are not started in this case.

Experimental Options

Process synchronisation method (-s | -tb | -tr)

With this options different mechanisms for process synchronisation can be selected. This can result in better spin performance for some models. The default synchronisation method (use no option) should be the best for most models.

Additional information

We tested Hugo with XMI files of UML models, which 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 as concurrent composite state. All its substates (that need to be non-concurrent composite states) are considered as orthogonal regions.
For CASE-tools that do not support choice pseudostates, you can use an empty composite state that contains the text '(choice)' instead.
If your CASE-tool doesn't support the specification of do-activities, you may start an entry-action with do/. Hugo will treat such an entry-action as a do-activity. Note, that a state can't have an entry-action and a do-activity at the same time in this case.
If a state should defer an event, you must add a tagged value to the state with the tag 'defer' and the name of the event as value.
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.
Concurrent regions may not have any incoming or outgoing transitions.

Currently unsupported UML constructs:

internal transitions
signal hierarchies
synch states
deep history states
change events
time events

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