Analysis Browser friendly
version
Back to Contents
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.

See also:

Languages | Configuration


(C) 2004 DARTS, IT Dept, CS, Uppsala University, Sweden