| News |
|
Beta Version
 Times 1.3 Beta now available online! Download here.
|
|
Times User Group
Has been created on YahooGroups! Register now!
|
|
Tool Paper
Presented at TACAS'02, received
ETAPS'02
Best Tool Demo Award.
Available here.
|
|
Background Paper
Presented at TACAS'02.
Available here. |
Last update:
Thursday, 06 Nov 2008, 10:26:39
|
|
Optimized for:
Mozilla/5.0
MSIE/6.0+
|
|
The Times Tool
Times - A Tool for Modeling and Implementation
of Embedded Systems.
It is a tool set for modelling, schedulability analysis, synthesis of (optimal) schedules
and executable code.
It is appropriate for systems that can be described as a set of tasks which are
triggered periodically or sporadically by time or external events.
 Click here for more screenshots...
Currently Times supports system specification, system analysis and code generation
for LegoOS platform.
A system specification in Times consists of three parts:
the control automata modelled as a network of timed automata extended
with tasks, a task table with information about the processes triggered
(released) when the control automata changes location, and a scheduling policy.
|
Main Features
-
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
completed.
-
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
LegoOS 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.
|
