25.10.2007

Generowanie automatów czasowych dla systemów czasu rzeczywistego

Komercyjne systemy czasu rzeczywistego są projektowane głównie w językach wysokiego poziomu, wspomaganych przez narzędzia ułatwiające ich testowanie, symulację, czy generowanie kodu wykonywalnego, ale rzadko wspierające ich formalną weryfikację. Z drugiej strony duża część badań w tej dziedzinie dotyczy opracowania i rozwijania metod weryfikacji dla modeli takich jak automaty czasowe i sieci Petriego z czasem. Intensywny rozwój przeżywają zwłaszcza metody weryfikacji modelowej automatów czasowych. Aby móc zastosować metody i narzędzia weryfikacji modelowej automatów czasowych do sprawdzania poprawności systemów czasowych, opisanych w językach wysokiego poziomu, proponujemy dokonać tłumaczenia z tych języków do automatów czasowych. W tym celu wprowadzamy reprezentację pośrednią, tak zwany język bazowy. Generowanie automatów odbywa się w dwóch krokach. Najpierw opis systemu w danym języku jest tłumaczony do reprezentacji pośredniej, a z niej do automatów czasowych. Na pierwszy krok powinny się składać przekształcenia wyłącznie syntaktyczne, dlatego język bazowy musi być wystarczająco bogaty, aby umożliwić wyrażanie istotnych aspektów komunikacji i synchronizacji systemów współbieżnych z ograniczeniami czasowymi. W czasie referatu zostanie przedstawiony język bazowy i metody generowania automatów czasowych dla programów w języku bazowym.

Istotnym problemem w praktycznym wykorzystaniu metod weryfikacji modelowej jest wykładnicza eksplozja liczby stanów modelu. Pokażemy w jaki sposób stosując statyczną analizę programu można uzyskać abstrakcyjny modelu systemu. Proponowana metoda jest oparta na technice cięcia programów (ang. program slicing). Abstrakcja zachowuje prawdziwość formuł logiki temporalnej CTL*_X, to jest CTL* bez operatora następnego kroku i jest uzależniona od weryfikowanej własności.