The modelling language of UPPAAL can quite naturally be extended with a subset
of the C programming language.
Most of this has now been implemented in the development branch. If you want to
try it, you can download the latest UPTA version of UPPAAL at
The UPTA version is based on the development and hence also contains support for
a C like constructs.
I'm closing this bug, as most of this is implemented in UPPAAL 3.5. Things like switch, break and continue
are missing, but specific bugs for those missing features should be created.