This case study is based on the Hubble space telescope lifetime (as found on the CADP website). It was translated from Aldebaran graph format to Reactive Module Language (RML) Continuous Time Markov Chain (CTMC).
The Hubble model:
Important!
// Hubble space telescope lifetime
// Holger Hermanns, Christophe Joubert, Hubert Garavel, and Wendelin Serwe
// Translated from ALDEBARAN to RML
ctmc
module M
x:[0..8] init 0;
[FAIL] x=0 -> 0.6 : (x’=1);
[FAIL] x=1 -> 0.5 : (x’=2);
[FAIL] x=2 -> 0.4 : (x’=3);
[FAIL] x=3 -> 0.3 : (x’=4);
[FAIL] x=4 -> 0.2 : (x’=5);
[SLEEP] x=4 -> 100 : (x’=7);
[FAIL] x=5 -> 0.1 : (x’=6);
[SLEEP] x=5 -> 100 : (x’=8);
[REPAIR] x=7 -> 6 : (x’=0);
[FAIL] x=7 -> 0.2 : (x’=8);
[REPAIR] x=8 -> 6 : (x’=0);
[FAIL] x=8 -> 0.1 : (x’=6);
endmodule
label “crash” = x=6;
label “sleep” = x=7 | x=8;
Download hubble.plasma
We have model checked the following property, meaning that a crash doesn’t occurs for 100 years.
Important!
//Liveness property.G<=100 !”crash”
Using our sequential algorithm with parameters set as
- alpha = 0.001 False positives probability
- beta = 0.001 False negatives probability
- delta = 0.001 Indifference region
- proba = 0.99 Probability
This means that we wanted to know if the probability that the property holds was superior to 99% with a fairly low probability of making an error.
The answer was computed as true in 0.952 seconds using 9239 simulations.
