Publikace na Matematicko-fyzikální fakulta |
2007
Abstrakt
Použití softwarových komponent je moderní přístup k vytváření rozšiřitelných a spolehlivých aplikací. Pro zajištění vysoké spolehlivosti by komponentová aplikace měla podstoupit verifikaci, například model checking, aby byly dokázány některé její vlastnosti.
Vlastní implementace je však obyčejně velmi složitá, a tak je nutné použít nějakou její abstrakci. Behavior protocols jsou vhodnou abstrakcí pro modelování chování softwarových komponent.
V tomto článku navrhujeme novou metodu pro verifikaci tohoto formalismu prostřednictvím transformace modelu do modelovacího jazyka Promela, který se dá následně ověřit nástrojem Spin. Takto je možné verifikovat nejen absenci komunikačních chyb, ale i vlastnosti zapsané v jazyku LTL.