is a modelling and schedulability analysis
tool for embedded real-time systems, developed at Uppsala University. It is appropriate
for systems that can be described as a set of preemptive or
non-preemptive tasks which are triggered periodically or sporadically
by time or external events. It provides a graphical interface for
editing and simulation, and an engine for schedulability analysis.
The main features of Times
- A graphical editor for timed automata extended with tasks, which
allows the user to model a system and the abstract behaviour of its
environment In addition the user may specify a set of preemptive or
non-preemtive tasks with parameters such as (relative) deadline,
execution time, priority, etc.
- A simulator, in which the user can validate the dynamic behaviour of
the system and see how the tasks execute according to the task
parameters and a given scheduling policy. The simulator shows a
graphical representation of the generated trace showing the time
points when the tasks are released, invoked, suspended, resumed, and
- A verifier for schedulability analysis, which is used to
check if all reachable states of the complete system are
schedulable that is, all task instances meet their deadlines.
A symbolic algorithm has been developed based on the
DBM techniques and implemented based on the verifier
of the Uppaal tool.
- A code generator for automatic synthesis of C-code on brickOS
platform from the model. If the automata model is schedulable
according to the schedulability analyser the execution of the
generated code will meet all the timing constraints specified in the
model and the tasks.
More information about TIMES can be found on the web site