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 (at)


Current version 0.8a (28.10.2015)

For obtaining the source code, please send an e-mail to knapp (at)

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