The
Times tool supports two kinds of analysis:
schedulability analysis and
verification of properties specified by temporal formulas.
Schedulability analysis
The schedulability analysis in
Times tool
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
Run->Schedulability analysis
. When the computation is
finished the property
schedulability
is shown to be
SATISFIED
or
NOT SATISFIED
.
Schedulability Property is SATISFIED
|
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
Show WCRT
button or use menu
Window->Response
times
to open a window showing worst case response times.
Worst Case Response Times
|
Verification
Using the verification you can check properties of your system specified by
temporal formulas. The complete syntax of the formulas is given in the
Languages chapter.
To run verification select the menu item
Run->Verification
.
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
own property.
Entering a Property
|
Click
OK
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
or
MAYBE SATISFIED
if
Over Approximation or
Under Approximation
was used (see
Configuration chapter for
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
Show trace
button.
The same holds for the traces generated while verifying "
E<>" and
"
A[] not" properties.