Ludwig-Maximilians-Universität, München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
http://www.pst.informatik.uni-muenchen.de/projekte/hugo/index.html

Hugo/RT

Hugo/RT is a UML model translator for model checking, theorem proving, and code generation: A UML model containing active classes with state machines, collaborations, interactions, and OCL constraints can be translated into the system languages of the real-time model checker UPPAAL, the on-the-fly model checker SPIN, the system language of the theorem prover KIV, and into Java and SystemC code.

For feedback, criticism and suggestions, please send an e-mail to knapp@pst.ifi.lmu.de.


Contents


Usage

There are two ways to use Hugo/RT: A basic mode, where all features are called manually, and a batch mode for model checking handling translation, verification, and retranslation of results.

  1. In basic mode, Hugo/RT is called as follows:

    hugort [options] [trail[.tl]] [model[.xmi|.xml|.ute|.zargo|.zip]]

    The options are described below.

    A trail file is an example run as generated by verifyta when called with the options -t [0|1|2] -q -s (UPPAAL), or spin when called with the options -l -g -w -v (SPIN).

    A model file can be of the following input formats:

    If no trail file and no model file are given, model input is accepted from stdin. The model file can be replaced by - in order to let Hugo/RT accept model input from stdin. Hugo/RT makes a best-effort guess to find out the input format.

  2. In batch mode, Hugo/RT is called as follows:

    hugort (spin|uppaal) [options] [model[.xmi|.xml|.ute|.zargo|.zip]]

    The options are described below, the model is handled as in basic mode.

    With the call hugort spin ..., Hugo/RT first translates the model according to the options into Promela and, if necessary, an LTL formula, performs model checking with SPIN, and retranslates the example trail of SPIN, if any, into a UML run. Similarly, with the call hugort uppaal ..., Hugo/RT does the analogous with UPPAAL. Currently, batch mode is available for UNIX systems only, as it is handled by a bash script.

Before any translation action is taken according to the options, the model is read into an internal representation and checked for inconsistencies. In particular, Hugo/RT type checks all guards and effects of state machines and the messages of interactions; all events occuring in triggers are checked for declaration; all attribute settings in objects and all constant settings in classes are type checked; &c. If any test fails, an error is issued and Hugo/RT exits.

Command line options

-o[uppaal|promela|kiv|java|systemc|smile|ute|dot|idadot|trail[=filename]]
--output[uppaal|promela|kiv|java|systemc|smile|ute|dot|idadot|trail[=filename]]

Translate UML model into a system of timed automata for UPPAAL or a Promela file for SPIN or a specification for KIV or Java code or SystemC code or a system of Smile machines or a UTE model or a GraphViz dot file of the state machines or a GraphViz dot file of the interactions. Also, a trail generated by the UPPAAL or the SPIN model checker can be retranslated into a UML run.

If filename is given, the result of the (re-)translation is put into a file filename; if additional output files are produced filename without its extension is used as the base file name. If no filename is provided, a base file name on the basis of the input file name (i.e., the input file name without its extension) is chosen; if the input is from stdin, the base file name is stdin.

For a translation into Java code, the base filename is taken to be a directory.

The base file name is extended by the extensions

.ta for the UPPAAL system file
.q for the UPPAAL query file
.pml for the SPIN Promela file
.ltl for the SPIN LTL file
.kiv for the KIV theory file
.smile for the Smile machines file
.ute for the UTE file
.dot for the dot file
.utl for UML runs

For retranslating an UPPAAL or a SPIN trail a trail has to be given.

Any number of -o options can be specified, but only the last option for a specific output format will be in effect.


-c[=name]
--collaboration[=name]

Create objects for collaboration name.

If no collaboration name exists in the UML model, a warning is issued and, if the UML model shows at least one collaboration, some collaboration is chosen, or, if there is no collaboration in the UML model, then the empty collaboration is chosen.

If no name is given, some collaboration in the UML model is chosen. If there is no collaboration in the UML model, a warning is issued and the empty collaboration is chosen.

If neither this option nor the -i option is used, no objects will be created.

This option is only considered when translating into UPPAAL or SPIN.


-i[=name]
--interaction[=name]

Create an observer for interaction name in a collaboration.

The collaboration is chosen according to the setting of the -c option. If the -c option is not used explicitly, use of the -c option without name is assumed.

If no interaction name exists in the collaboration, a warning is issued and, if the collaboration shows at least one interaction, some interaction is chosen, or, if there is no interaction in the collaboration, then the empty interaction is chosen.

If no name is given, some interaction in the collaboration is chosen. If there is no interaction in the collaboration, a warning is issued and the empty interaction is chosen.

This option is only considered when translating into UPPAAL or SPIN.


-a[=name]
--assertion[=name]

Translate assertion name in a collaboration.

The collaboration is chosen according to the setting of the -c option. If the -c option is not used explicitly, use of the -c option without name is assumed.

If no assertion name exists in the collaboration, a warning is issued.

If no name is given, some assertion in the collaboration is chosen. If there is no assertion in the collaboration, a warning is issued and the assertion EF true is chosen for UPPAAL and F true for SPIN.

This option is only considered when translating into UPPAAL or SPIN.


-d=int
--maxDelay=int

Set the maximum delay of the network.

A warning is issued if the delay is negative and the default delay is chosen. The default delay is 10.

This option is only considered when translating into UPPAAL and the network capacity is greater than zero.


-n=int
--networkCapacity=int

Set the capacity of the network.

A warning is issued if the capacity is negative and the default capacity is chosen. The default network capacity is 2.

If the network capacity is set to 0 the network delay set by the -d option is not taken into account.

This option is only considered when translating into UPPAAL.


-q=int[,int[,int]]
--queueCapacity=int[,int[,int]]

Set the capacities of the external (events from the network), internal (completion and time events), and deferred event queues, respectively.

If only a single integer value is provided, only the capacity of the external event queue is set; if only two integer values are provided, only the capacities of the external and the internal event queue are set.

A warning is issued if any capacity is not positive and the corresponding default capacity is chosen. The default capacities are: 5 for the external event queue, 2 for the internal event queue, and 2 for the deferred event queue.

This option is only considered when translating into UPPAAL or SPIN.


-k[=(true|false)]
--centralNetwork[=(true|false)]

Generate a single, central network for all object communications. By default, the external queue of each object is combined with a network.

This option is only considered when translating into UPPAAL.


-b=int,int
--intBounds=int,int

Set lower and upper bounds for integers. By default, the lower bound is -32768, the upper bound 32767.

This option is only considered when translating into UPPAAL.


-x[=(true|false)]
--mutex[=(true|false)]

Include a mutex for mutually excluded object executions.

This option is only considered when translating into UPPAAL or SPIN.


-m[=(true|false)]
--smileMachine[=(true|false)]

Force Smile-based translation.

Even if this option is not set, a Smile-based translation is used if some class of the UML model shows operations. If this option is not set and no class of the UML model shows operations, state machines with the following characteristics are translated using a flattening scheme: The state machine does not contain semantic pseudo-states (i.e. choice pseudo-states or initial pseudo-states targeting junction pseudo-states) and the state machine does not contain wait transitions.

This option is only considered when translating into UPPAAL.


-r[=(true|false)]
--fixedOrderRegions[=(true|false)]

Use deterministic ordering of regions.

If this option is not set, the generated code will consider all possible ways of choosing transitions in orthogonal regions. If this option is set, a fixed, random ordering in which the orthogonal regions are considered is chosen.

This option is only considered for Smile-based translations.


-t[=(true|false)]
--fixedOrderTransitionFiring[=(true|false)]

Use deterministic ordering of transitions.

If this option is not set, the generated code will consider all possible permutations of executing actions in orthogonal regions (entry actions and effects). If this option is set, a fixed, random ordering for executing actions in orthogonal regions is chosen.

This option is only considered for Smile-based translations.


-p[=(true|false)]
--phaseBased[=(true|false)]

Use a phase-based translation for interactions.

If this option is not set, a bit-array scheme for storing the event history in interactions is used.

This option is only considered when translating into UPPAAL or SPIN.


-v[=(true|false)]
--verbose[=(true|false)]

Produce verbose output.

In verbose mode, when converting a UML model to its internal representation, all modifications to the UML model due to the internal representation are reported.


-s[=(true|false)]
--silent[=(true|false)]

Silent mode, but showing warnings and errors.


-V
--version

Show version of Hugo/RT and exit.


-h
--help

Show a short usage text and exit.


-D
--debug

Debugging mode. Currently not in use.



UML Models

Hugo/RT reads UML models in either XMI 1.0-1.2 or UTE format.

In XMI, all UML state machines must be specified in the context of a UML class. Each UML class has to declare all call and send events, which its state machine can handle: If a class declares an operation with name m and input kind parameters p1,...,pn with types τ1,...,τn, then it can receive call events of the form m(v1,...,vn). If a class declares a reception for the signal s with attributes p1,...,pn with types τ1,...,τn, then it can receive send events of the form s(v1,...,vn).

Workarounds

There are several workarounds for UML CASE tools that do not support the full range of features available in Hugo/RT:

In some cases it may be preferable, to translate an XMI UML model into UTE first and then to work with the UTE model representation.

Restrictions

Some UML features are currently not handled correctly by Hugo/RT:


Grammar for Expressions, Statements, and Constraints

The guards in state machines must be (boolean) expressions (Expr), the effects in state machines must be statements (Stm), model constraints must be constraints (Constr) according to the following grammar:

Id ::= Name |                                                      -- local reference
       Name ["." Id]                                               -- global reference

Expr ::= Expr "?" Expr ":" Expr                                    -- conditional
       | Expr ("||" | "&&") Expr                                   -- boolean connectives
       | "!" Expr                                                  -- negation
       | Expr ("<" | "<=" | "==" | "!=" | "=>" | ">") Expr         -- relations
       | Expr ("+" | "-" | "*" | "/" | "%") Expr                   -- arithmetic
       | ("+" | "-") Expr                                          -- unary
       | "(" Expr ")"                                              -- parentheses
       | Id                                                        -- identifiers
       | "this" | "self"                                           -- self reference
       | "null"                                                    -- null reference
       | "true" | "false"                                          -- booleans
       | Int                                                       -- integer

Stm ::= Stm "::" Stm                                               -- non-deterministic choice
      | Stm "||" Stm                                               -- parallel composition
      | Stm ";" Stm                                                -- sequential composition
      | "if" "(" Expr ")" Stm ["else" Stm]                         -- conditional
      | "{" Stm "}"                                                -- block
      | "assert" "(" Expr ")" ";"                                  -- assertion
      | Id["[" Expr "]"] "=" Expr ";"                              -- (array) assignment
      | [^] ["this" "."] Id "(" [Expr {"," Expr}] ")" ";"          -- signal/method invocation on self
      | [^] Id["[" Expr "]"] "." Id "(" [Expr {"," Expr}] ")" ";"  -- (array) signal/method invocation
      | ";"                                                        -- skip

Constr ::= TCTLConstr | LTLConstr

TCTLConstr ::= ("AG" | "AF" | "EG" | "EF") Frm                     -- (timed) CTL constraint

LTLConstr ::= "F" LTLConstr                                        -- (untimed) LTL constraint
            | "G" LTLConstr
            | LTLConstr "U" LTLConstr
            | Frm

Frm ::= Frm ("and" || "or" || "implies") Frm                       -- boolean connectives
      | "not" Frm                                                  -- negation
      | Name "." "inState" "(" Id ")"                              -- in state
      | Expr                                                       -- expressions
      | "deadlock"                                                 -- deadlock
      | "fail"                                                     -- failure

Several context and typing conditions apply. We only list some important restrictions:


Textual UML Format (UTE)

The proprietary UML text format UTE reflects all UML features that are handled by Hugo/RT.

Model ::= "model" Name "{"
            [Properties] {Class} {Collaboration}
          "}"
          
Properties ::= "properties" "{"
                 ["networkCapacity" "=" Nat ";"]
                 ["centralNetwork" "=" Nat ";"]
                 ["networkDelay" "=" Nat ";"]
                 ["externalQueueCapacity" "=" Nat ";"]
                 ["internalQueueCapacity" "=" Nat ";"]
                 ["deferredQueueCapacity" "=" Nat ";"]
                 ["mutex" "=" ["true" | "false"] ";"]
                 ["smileMachine" "=" ["true" | "false"] ";"]
                 ["fixedOrderRegions" "=" ["true" | "false"] ";"]
                 ["fixedOrderTransitionFiring" "=" ["true" | "false"] ";"]
                 ["phaseBased" "=" ["true" | "false"] ";"]
               "}"

Class ::= "class" Name "{"
            [Signature] [Behaviour]
          "}"

Signature ::= "signature" "{"
                {(Constant | Attribute | Operation | Reception)}
              "}"
Constant ::= ["static"] "const" Name ":" TypeName ["[" Expr "]"] "=" Expr ";"
Attribute ::= ["static"] "attr" Name ":" TypeName ["[" Expr "]"] ["=" Expr] ";"
Operation ::= "operation" Name "(" [Name ":" TypeName {"," Name ":" TypeName}] ")" ";"
Reception ::= "reception" Name "(" [Name ":" TypeName {"," Name ":" TypeName}] ")" ";"

Behaviour ::= "behaviour" "{"
                "states" "{" {State} "}
                "transitions" "{" {Transition} "}"
              "}"

State ::= PseudoState |
        | "final" Name ";"
        | "simple" Name (("{" [Defer] [Entry] [Exit] "}") | ";")
        | CompositeState
PseudoState ::= "initial" Name ";"
              | "junction" Name ";"
              | "choice" Name ";"
              | "fork" Name ";"
              | "join" Name ";"
              | "history" Name ";"
CompositeState ::= "composite" Name "{" [Defer] [Entry] [Exit] {State} "}"
                 | "concurrent" Name "{" [Defer] [Entry] [Exit] {CompositeState} "}"

Defer ::= "defer" EventName {"," EventName}
Entry ::= "entry" Stm
Exit ::= "exit" Stm

Transition ::= StateId "->" StateId (("{" [Trigger] [Guard] [Effect] "}") | ";")
Trigger ::= "trigger" "after" "[" Expr ["," Expr] "]"
          | "trigger" "wait"
          | "trigger" EventName
Guard ::= "guard" Expr
Effect ::= "effect" Stm

Collaboration ::= "collaboration" Name "{"
                    [Properties] {Object} {Interaction} {Assertion}
                  "}"

Object ::= "object" Name ":" ClassName "{"
             {Slot}
           "}"
Slot ::= AttributeName "=" (Expr | "{" Expr {"," Expr} "}") ";"

Interaction ::= "interaction" Name "{"
                  {Message} {InteractionFragment} [Timings]
                "}"
Message ::= [Name ":"] ObjectName "->" ObjectName ":" BehaviouralName "(" Expr {"," Expr} ")" ";"
InteractionFragment ::= BasicInteraction
                      | StateInvariant
                      | CombinedFragment
BasicInteraction ::= "basic" "{"
                       {Lifeline}
                     "}"
Lifeline ::= ObjectName "{"
               Occurrence [ "after" {Occurrence}+ ] ";"
             "}"
Occurrence ::= ("snd" | "rcv") "(" MessageName ")"
StateInvariant ::= "invariant" "<" ObjectName {"," ObjectName}* ">"
CombinedFragment ::= "loop" "<" (Integer "," (Integer | "infty")) | "infty") "{" BasicInteraction "}"
                   | "not" "{" BasicInteraction "}"
                   | ("seq" | "strict" | "par" | "alt") {InteractionOperand}+
                   | "opt" InteractionOperand
                   | "ignore" "<" MessageName {"," MessageName} ">" InteractionOperand
                   | "sloop" "<" (Integer "," (Integer | "infty")) | "infty") InteractionOperand
InteractionOperand ::= ["[" Expr "]"] "{" {InteractionFragment}+ "}"
Timings ::= "timing" "{" {Timing}+ "}"
Timing ::= Occurrence "-" Occurrence ("<" | "<=") Expr

Assertion ::= "assertion" Name "{"
                 Constr
              "}"

TypeName ::= "int" | "bool" | "clock" | ClassName  -- name of a primitive type or a class type
ClassName ::= Name                                 -- name of a class
AttributeName ::= Name                             -- name of an attribute
BehaviouralName ::= Name                           -- name of an operation or a reception
EventName ::= Name                                 -- name of an operation or a reception
ObjectName ::= Name                                -- name of an object
MessageName ::= Name                               -- name of a message
StateId ::= Id                                     -- identifier of a state


Download

For obtaining the source code, please send an e-mail to knapp@pst.ifi.lmu.de.

This software includes software developed by the Apache Software Foundation and by Novosoft.


People

The development of Hugo/RT is led by Alexander Knapp (Ludwig-Maximilians-Universität München) and Stephan Merz (LORIA/INRIA Nancy). The current release of Hugo/RT has been integrated by Alexander Knapp.

Hugo/RT is based on ideas and source code by


Publications


Release history

0.51a (08/08/11)
FIX: Translation of history states could result in stack overflow (thanks to Elisabeth Wolf).
FIX: Access to states in UPPAAL queries was handled like field access.
FIX: In flat UPPAAL translation fetching states were "committed" instead of "urgent".
0.50a (06/07/28)
Translation of UML 2.0 interactions for SPIN and UPPAAL; visualisation of intermediate interaction automaton by -oidadot.
Translation into SystemC code.
Rewrite of XMI parsing; the parser does not rely on an XMI-library, but only searches for keywords.
Integer bounds for UPPAAL translation.
FIX: Mutexes could produce deadlocks, when events were to be put into a full queue.
0.49 (06/01/16)
Hugo/RT now uses Java 5.
FIX: The retranslation of SPIN trail did not recognise the :init: process.
FIX: There was an error in assigning completion numbers to completion states: Numbers were reused in regions such that a join could take a state to be completed, although it only shared the same completion number with some other state.
FIX: Removed "anonymous labels" for cycles in Java translation.
FIX: Removed possiblity of duplicate labels in Smile.
FIX: The Promela identifier generation didn't take into account that macro names break the block structure.
0.42 (05/03/05)
The -odot option now produces graph information of the UML state machines in the model.
FIX: The retranslation of SPIN trail did not recognise the final system state (thanks to Philipz).
0.41 (05/02/02)
FIX: The Java translation produced unreachable code.
FIX: In the Java translation, insertion of an event into the event queue could lead to a deadlock.
FIX: In the Java translation, the EventQueue.debug()-method was called statically.
0.40 (05/01/23)
Retranslation of SPIN trails.
Integration of Smile-based Java code generation.
FIX: Negation of identifier expressions was incorrect (thanks to Alik Harhurin).
FIX: Deferred events in the flattening UPPAAL translation have not been considered again.
FIX: The translation of deadlock was incorrect, if no state machine shows a final state.
0.32 (04/08/29)
Retranslation of UPPAAL trails.
Combination of queues and network.
Performance improvements for UPPAAL by resetting unused clocks.
Optional mutex added to UPPAAL and made optional for Spin.
Change in constraint format for selectively translating assertions.
FIX: Completion events for joins have led to an overflow of the internal event queue, if there is a loop of reactivations of the completed state.
0.31 (04/07/25)
Atomic blocks added to Smile for more efficient Spin code.
FIX: When checking for deadlocks in UPPAAL, terminated state machines have not been taken into account.
0.30 (04/04/11)
First official release of Hugo/RT.

Previous releases

The Promela code generation possiblities of release Hugo 3.00 are covered by Hugo/RT. The Promela code generation of Hugo 2.00 uses an interpreting approach, which has been rendered obsolete. However, both Hugo 2.00 and Hugo 3.00 feature Java code generation using the interpretative approach which is currently not included in Hugo/RT; an alternative Smile-based Java code generation procedure has been introduced in Hugo 0.40.

The first release of an extension of Hugo by real-time features, RT Hugo 0.5, is now obsolete; its features can be mimicked by using the flattening translation scheme of Hugo/RT for UPPAAL code generation.

Hugo/RT is model (XMI) compatible with the previous versions, in as far as no Java code is used.


List of all projects Chair Department University
Alexander Knapp (11.4.4)
Last modified: Mon Aug 08 17:49:35 CEST 2008