Ludwig-Maximilians-Universität, München, Institut für InformatikHugo/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.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.
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:
.xmi or .xml).zip).zargo).ute)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.
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.
-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.
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).
There are several workarounds for UML CASE tools that do not support the full range of features available in Hugo/RT:
receive; the name of the first input parameter of such an operation is interpreted as the name of the signal, its remaining input parameters as the attribute declarations of this signal.(concurrent) in its name. All its substates (that need to be non-concurrent composite states) are considered as orthogonal regions.(choice) in its name.defer and the name of the event as value.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.
Some UML features are currently not handled correctly by Hugo/RT:
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:
Id in an assignment must denote a non-constant local or a global name, i.e. an non-constant attribute of the surrounding class or a non-constant static attribute of some class. Id in a sending of an operation call or in a raising of a signal must denote a local or a global name, i.e. an attribute of the surrounding class, a static attribute of some class, or a parameter name of the triggering event. Expr. this and self cannot be used in constraints. Name in an "in state" formula must denote an object. Id in an "in state" formula must denote a state machine state of the object named by Name (using the "." notation). if, else, this, self, null, true, false. 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
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.
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
-oidadot.
-odot option now produces graph information of the UML state machines in the model.
EventQueue.debug()-method was called statically.
deadlock was incorrect, if no state machine shows a final state.
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