Re: Dostepnosc systemu - metody formalne - Grupy dyskusyjne w eGospodarka.pl

eGospodarka.pl › Grupy › pl.comp.programming › Dostepnosc systemu - metody formalne › Re: Dostepnosc systemu - metody formalne

Path: news-archive.icm.edu.pl!news.icm.edu.pl!news.nask.pl!news.nask.org.pl!news.uni-
stuttgart.de!news.belwue.de!news.osn.de!diablo2.news.osn.de!195.114.241.69.MISM
ATCH!feeder.news-service.com!postnews.google.com!h17g2000yqn.googlegroups.com!n
ot-for-mail
From: Michał Knapik <o...@g...com>
Newsgroups: pl.comp.lang.c,pl.comp.programming
Subject: Re: Dostepnosc systemu - metody formalne
Date: Sat, 23 Jul 2011 15:48:53 -0700 (PDT)
Organization: http://groups.google.com
Lines: 26
Message-ID: <9...@h...googlegroups.com>
References: <9...@y...googlegroups.com>
NNTP-Posting-Host: 62.121.86.20
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1311461779 14702 127.0.0.1 (23 Jul 2011 22:56:19 GMT)
X-Complaints-To: g...@g...com
NNTP-Posting-Date: Sat, 23 Jul 2011 22:56:19 +0000 (UTC)
Complaints-To: g...@g...com
Injection-Info: h17g2000yqn.googlegroups.com; posting-host=62.121.86.20;
posting-account=_i_xoQoAAACaI_y6fUQPN03S4BBPwFx7
User-Agent: G2/1.0
X-Google-Web-Client: true
X-Google-Header-Order: HNKRUAELSC
X-HTTP-UserAgent: Mozilla/5.0 (Windows NT 6.1; WOW64) AppleWebKit/534.30 (KHTML, like
Gecko) Chrome/12.0.742.122 Safari/534.30,gzip(gfe)
Xref: news-archive.icm.edu.pl pl.comp.lang.c:295633 pl.comp.programming:191648
[ ukryj nagłówki ]
On 17 Lip, 21:40, Seweryn Habdank-Wojewódzki <h...@g...com>
wrote:

> Czy znacie jakis soft lub pomoce do obliczania tudziez formalnego
> potwierdzania dostepnosci (availability) systemow rozproszonych?

Model Checking - narzędzia takie jak nuSMV, UPPAAL i parę innych.

> W ubezpieczeniach i w technice oblicza sie prawdopodobienstwa choroby
> lub uszkodzenia sie jakiegos podzespolu.
> Zaczalem sobie powolutku rozpisywac rownanka, ale jesli system jest
> zlozony z trzech elementow zaczyna juz byc skomplikowany
> do liczenia na papierku.
>
> Moze ktos sie bawil w udowadnianie, ze po czasie T system bedzie
> dzialal z jakim tam prawdopodobienstwem.
> Albo calkowicie inzyniersko, jak udowodnic, ze dostepnosc
> rozproszonego systemu wynosi np. 99.7%.

Niestety nuSMV i UPPAAL dają tylko odpowiedzi w rodzaju: "tak, system
będzie dostępny dla każdego przebiegu". Nie znam się na
probabilistycznym MC, ale wiem że jest do tego narzędzie:
http://www.prismmodelchecker.org/.

Pozdrav.
M.