Embedded Control Example - Advanced Version

From AadlWiki

Jump to: navigation, search

This is an advanced version of the first embedded control example. If you are not familiar with AADL and the error model annex, please read it before. In particular, it shows the overall architecture view with its error propagations.


Additional model information

System Analysis

Time before the bus reach one failure mode

The following property check for the proability of a failure of the bus (first occurrence). As the bus is in the failure mode once a processor has a transient error, we might expect the same value as the the transient failure of a processor in the previous example.

P=? [ true U<=T*3600*24 (bmain_i_instance_is_failed) ]


Time of bus failure

One idea is to see how long the shared bus is in the failure mode. Because of the bus switches into the failure mode because of a transient failure of a processor, the cumulative value might be interesting to analyse.

First, we add a reward in the model to record a bus failure. Each time we reach the failure mode, we increment the reward.

rewards "bus_failure"
    bmain_i_instance_is_failed : 1;

Then, we define a property that show the cumulative reward value over time. The following property would show the reward value for a given amount of time.

R{"bus_failure"}=? [ C<=T*3600*24 ]

Cumulative time in Transient Failure

rewards "one_processor_transient"
    (pomain_i_instance_is_transientfailure) | (pimain_i_instance_is_transientfailure) | (pomain_i_instance_is_transientfailure)  : 1;
R{"one_processor_transient"}=? [ C<=T*3600*24 ]


Personal tools