tool supports two kinds of analysis:
of properties specified by temporal formulas.
The schedulability analysis in Times
is based on the reachability analysis of the scheduler automaton that is
constructed according to the chosen scheduling policy.
An automaton is schedulable if there exists a (preemptive or
non-preemptive) scheduling strategy such that all possible sequences
of events accepted by the automaton are schedulable in the sense
that all associated tasks can be computed within their deadlines.
To run the Schedulability analysis select the menu item
. When the computation is
finished the property
is shown to be
Schedulability Property is
Once schedulability analysis has been performed and the result is positive
you can observe the Worst Case Response Times (WCRT) of the tasks in the
system. Click on the
button or use menu
to open a window showing worst case response times.
Worst Case Response Times
Using the verification you can check properties of your system specified by
temporal formulas. The complete syntax of the formulas is given in the
To run verification select the menu item
In the dialog that appears you can select a predefined property (read from the
.q file, which has the same name as the name of the .xml file), or write your
Entering a Property
to check the specified property. A result
dialog appears, with a progress bar. When the progress completes,
the result is displayed as SATISFIED
, NOT SATISFIED
if Over Approximation
or Under Approximation
was used (see Configuration
information about configuring the verifier).
The Result of Property Checking
If the property has not been satisfied and there is a counterexample, you can load
the trace containing it into the simulator by pressing the
The same holds for the traces generated while verifying "E<>