22.01.2004

Testowanie osiągalności dla automatów czasowych za pomoca algorytmu podziału

Jednym z zagadnień rozwiązywanych za pomocą metod weryfikacji modelowej jest testowanie osiągalności, tj. badanie, czy system może kiedyś znaleźć się w stanie o określonych cechach. Wymaga to przejrzenia przestrzeni stanów systemu. Istotne znaczenie ma zatem jej rozmiar, który w niektórych przypadkach - np. występowania zależności czasowych - może być nawet nieskończony. Istnieje wiele technik umożliwiających weryfikację takich systemów. Należy do nich wykorzystanie skończonych struktur zachowujących testowane własności - tzw. modeli abstrakcyjnych.

W referacie zaprezentowana zostanie nowa metoda generowania modeli abstrakcyjnych dla automatów czasowych, bazująca na znanym algorytmie podziału (minimalizacji). Otrzymywane modele pseudosymulacyjne zachowują osiągalność, a przy tym mogą być mniejsze niż używane zazwyczaj do jej testowania tzw. grafy "forward-reachability". Możliwe jest ponadto wykonywanie weryfikacji "w locie", tj. przerywanie budowania modelu, gdy wygenerowany zostanie stan o zadanych cechach.

Wstępna implementacja metody stanowi cześć systemu weryfikacyjnego VerICS, opracowanego i rozwijanego w IPI PAN.