Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti
Diskusia k článku: Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti
Prispievajte do diskusií ako
prihlásený užívateľ.
Komentár, na ktorý odpovedáte:
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Re: Zial...
Od: still
|
Pridané:
2009-08-16 11:47:51
Neviem presne o aky druh verifikacie slo v tomto pripade, ale jednoduchy (spin) model checking je urceny na verifikaciu programov, ci uz single thread/process, ale aj paralelnych a distribuovanych systemov ;)
Tato verifikacia okrem liviness/starvation/deadlock chyb zistuje, ci je dany system (ne)schopny dosiahnut urcity stav/konfiguraciu a presne urcit akym sposobom tento stav nastal. Takze ti presne popise pripady ako k deadlocku doslo a nepotrebujes ziadny debug :)
A ak narazas cisto na moj zjednoduseny priklad, tak s deadlockom 2 strojov by mal pocitat ten softver. Ale kedze deadlock nemoze nastat (formalne dokazane) bude treba osetrit iny pripad, teda uplne vyradenie strojov z cinnosti, najjednoduchsie nejakym timeoutom na danu ulohu - ale to uz je ina vec (ktora sa taktiez da odchytit formalnou verifikaciou ;)
|
neprihlásený 