Templates

UPPAAL provides a rich language for defining templates in the form of extended timed automata. In contrast to classical timed automata, timed automata in UPPAAL can use a rich expression language to test and update clock, variables, record types, call user defined functions, etc.

The automaton of a template consist of Locations and edges. A template may also have local declarations and parameters. A template is instantiated by a process assignment (in the system definition).