Publikace na Matematicko-fyzikální fakulta |
2007
Abstrakt
V článku prezentujeme alternativní přístup k paralelní a distribuované verifikaci. Na rozdíl od metod, které stavový prostor rozdělují, my udržujeme stavy seřazené u sebe, které formují řetězec. Řetězec stavů je předáván mezi uzly v síti uspořádaných v logickém kruhu, kde každý uzel zpracovává řatězec vždy v místě, které právě vidí.
Metoda umí využít postavení stavů, ukládat stavy efektivně na externí úložistě a dobře škáluje v síti do desítek různorodých uzlů. Naimplementovali jsme prototyp, který potvrdil velmi dobré vlastnosti škálovatelnosti s počtem procesorů a uzlů při ověřování skutečných úloh.