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.