Publikace na Matematicko-fyzikální fakulta |
2010
Abstrakt
Klíčový problém v kompozičním model checkingu softwarových systémů je to, že typické model checkery příjímají pouze uzavřené systémy a proto jednotlivé komponenty nemohou být ověřeny přímo. Typické řešení je vytvořit umělé prostředí pro komponentu.
Pro praktické účely je dostatečné zachytit v prostředí jen použití komponenty v určitém systému – tato myšlenka je vyjádřena paradigmatem assume-guarantee. V tomto článku prezentujeme náš přístup k verifikaci softwarových systémů v kontextu platformy SOFA 2 podle paradigmatu assume-guarantee.
Ukazujeme přínos našeho přístupu na výsledcích experimentů s netriviálním softwarovým systémem.