On simulation methods for timed automata

In the paper the idea of timed automata simulator is introduced. The proposed simulator is an extension of the UPPAAL tool simulator. Instead of choosing transition to be performed randomly or manually, the simulator calculates transition times according to transition guard and state invariant for each transition. Described procedure can reveal realistic behavior of the system modeled by the automaton. To reach the target, an extension of timed automata formal is proposed. Within the paper the concept of a state-space tracing is shown on a case-study.