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: xman
|
Pridané:
2009-08-16 12:08:07
toto slo cez refinement z abstraktneho modelu na C-implementaciu v systeme Isabelle/HOL..
Mne islo o to, ze ked mas paralelny kod v komponentach,
tak musis uvazovat aj ine behavioralne vlastnosti ako
vstupne a vystupne podmienky pri imperativnom programovani...
|