{"id":1094,"date":"2013-10-10T11:22:26","date_gmt":"2013-10-10T09:22:26","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1094"},"modified":"2015-03-17T17:47:14","modified_gmt":"2015-03-17T16:47:14","slug":"hubble","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/hubble\/","title":{"rendered":"Hubble"},"content":{"rendered":"

This case study is based on the Hubble space telescope lifetime (as found on the CADP website). <\/i>It was translated from Aldebaran graph format to Reactive Module Language (RML) Continuous Time Markov Chain (CTMC).<\/p>\n

The Hubble model:<\/p>\n

Important!<\/strong><\/p><\/p>\n

\/\/ Hubble space telescope lifetime
\n\/\/ Holger Hermanns, Christophe Joubert, Hubert Garavel, and Wendelin Serwe
\n\/\/ Translated from ALDEBARAN to RML<\/p>\n

ctmc
\nmodule M
\nx:[0..8] init 0;
\n[FAIL] x=0 -> 0.6 : (x’=1);
\n[FAIL] x=1 -> 0.5 : (x’=2);
\n[FAIL] x=2 -> 0.4 : (x’=3);
\n[FAIL] x=3 -> 0.3 : (x’=4);
\n[FAIL] x=4 -> 0.2 : (x’=5);
\n[SLEEP] x=4 -> 100 : (x’=7);
\n[FAIL] x=5 -> 0.1 : (x’=6);
\n[SLEEP] x=5 -> 100 : (x’=8);
\n[REPAIR] x=7 -> 6 : (x’=0);
\n[FAIL] x=7 -> 0.2 : (x’=8);
\n[REPAIR] x=8 -> 6 : (x’=0);
\n[FAIL] x=8 -> 0.1 : (x’=6);
\nendmodule<\/p>\n

label “crash” = x=6;
\nlabel “sleep” = x=7 | x=8;<\/div>\n

Download hubble.plasma<\/strong><\/a><\/p>\n

We have model checked the following property, meaning that a crash doesn’t occurs for 100 years.<\/p>\n

Important!<\/strong><\/p>\/\/Liveness property.<\/p>\n

G<=100 !”crash”<\/p>\n

<\/div>\n

Using our sequential algorithm<\/strong> with parameters set as<\/p>\n