Strona domowa systemu
Verics (VerICS) jest oryginalnym polskim
weryfikatorem opracowanym i
rozwijanym w Instytucie Podstaw Informatyki Polskiej Akademii Nauk w
ramach projektów badawczych
Automatyczna weryfikacja systemów
zależnych od czasu i
Automatyczna symboliczna weryfikacja programów i protokołów
kryptograficznych w systemach rozproszonych. Początkowo system
przeznaczony był do weryfikacji automatów czasowych i protokołów
zapisanych w języku Estelle. Obecnie prowadzone prace mają na celu
rozszerzenie jego funkcjonalności.
Opis weryfikatora
Obecny stan systemu VerICS
obrazuje następujący schemat:
Wejściem dla Vericsa może być:
- specyfikacja w języku Estelle
(przykład)
- specyfikacja zapisana w naszym oryginalnym języku bazowym IL
(przykład)
- automaty czasowe zapisane w formacie akceptowanym przez
weryfikator Kronos
(przykład)
System umożliwia wykonanie translacji specyfikacji do
postaci automatów czasowych, które przekazywane są następnie
do kolejnych komponentów naszego narzędzia.
Verics pozwala obecnie na testowanie osiągalności. W celu wykazania, że
własność bezpieczeństwa (safety) nie zachodzi, stosowana jest
nowa bardzo efektywna metoda bazująca na translacji problemu osiągalności
dla automatów czasowych do problemu spełnialności formuł zdaniowych
(problemu SAT). Dowodzenie poprawności systemu wykonywane jest za pomocą
budowania abstrakcyjnego modelu systemu przy równoczesnym testowaniu
osiągalności w tym modelu stanu spełniającego żądaną własność.
Artykuły na temat systemu Verics:
- P. Dembiński, A. Janowska, P. Janowski, W. Penczek,
A. Półrola, B. Woźna, M. Szreter, A. Zbrzezny:
VerICS: A Tool for Verifying
Timed Automata and Estelle Specifications.
Proc. of the 9th Int. Conf. on Tools and Algorithms for
Construction and Analysis of Systems (TACAS'03). LNCS, vol. 2619,
str. 278-283,
©
Springer-Verlag, 2003.
ps.gz
- P. Dembiński, A. Janowska, P. Janowski, W. Penczek,
A. Półrola, B. Woźna, M. Szreter, A. Zbrzezny:
VerICS: weryfikator dla
automatów czasowych i specyfikacji zapisanych w
języku Estelle.
Materiały X Konferencji Systemy Czasu Rzeczywistego (SCR'03),
str. 17-26, Instytut Informatyki Politechniki Śląskiej, 2003.
ps.gz
- W. Nabiałek, A. Niewiadomski, W. Penczek,
A. Półrola, M. Szreter:
VerICS 2004: A Model Checker for
Real Time and Multi-agent Systems.
Proc. of the Int. Workshop
"Concurrency, Specification and Programming" (CS&P'04),
Informatik-Berichte 170(1), str. 88-99, Humboldt University, 2004.
pdf
Ostatnia aktualizacja:
21.07.2006