Publikace na Matematicko-fyzikální fakulta |
2005
Abstrakt
Automatické ověřování vlastností netriviálních komponentových aplikací produkuje dlouhé záznamy o průběhu výpočtů vedoucích k chybám. V tomto článku navrhujeme dva způsoby řešení problému lokalizace a ladění specifikace - vizualizace stavového protoru a anotace protokolů.