Weryfikacja formalna

fakultatywne

Języki, automaty i obliczenia 1000-214bJAO

Na kursie przedstawiona zostanie teoria formalnej weryfikacji i syntezy programów.

Przedstawione zostaną zagadnienia sprawdzania modeli (ang. model-checking) dla

systemów skończenie- i nieskończeniestanowych, dla oprogramowania i sprzętu,

dla czasu dyskretnyego i ciągłego oraz dla systemów deterministycznych i

stochastycznych.

1. Model-checking dla skończeniestanowych systemów reaktywnych. Logiki temporalne (LTL, CTL, CTL*), automaty Büchiego.

2. Symbolicze sprawdzanie modeli z użyciem BDD. Redukcje częściowo-porządkowe.

3. Dowodzenie terminacji programów za pomocą metod size-change termination.

4. Weryfikacja systemów czasu ciągłego z użyciem automatów czasowych.

5. Sprawdzanie stochastycznych modeli (ang. stochastic model-checking): weryfikacja dla łańcuchów Markowa czasu dyskretnego i ciągłego.

6. Sprawdzanie modeli nieskończeniestanowych: weryfikacja programów rekurencyjnych z użyciem automatów stosowych. Weryfikacja protokołów z kanałami komunikacyjnymi. Weryfikacja parametryzowana.

7. Sprawdzanie modeli dla hardware'u: weryfikacja układów kombinacyjnych i sekwencyjnych.

8. Synteza programów skończeniestanowych: problem Churcha i twierdzenie Büchi-Landwebera. Sterowanie Ramadge'a i Wonhama dla dyskretnych systemów zdarzeń.

Slajdy z wykładu i wybrane rozdziały następujących książek:

- Model Checking by Clarke, Grumberg, and Peled (1, 2)

- Principles of Model Checking by Baier and Katoen (1, 2, 4, 5)

- Handbook of Model Checking by Clarke, Henzinger, Veith, and Bloem (1, 2,

4, 5, 6, 8)

- Handbook of Automata Theory (8)

- Program termination analysis in polynomial time by Ben-Amram and Lee (3)

- Introduction to Formal Hardware Verification by Kropf (7)

Wiedza: absolwent zna i rozumie

- w pogłębionym stopniu - wiedzę z działów matematyki niezbędnych do

studiowania informatyki (K_W01)

- w pogłębionym stopniu - rolę i znaczenie konstrukcji rozumowań

matematycznych (K_W02)

Umiejętności: absolwent potrafi

- konstruować rozumowania matematyczne (K_U01)

- wyrażać problemy obliczeniowe w języku matematyki (K_U02)

- analizować pojęcia sformalizowane w wybranych systemach logicznych o

znaczeniu informatycznym, tworzyć w nich formalizacje zadanych pojęć bądź

też dowodzić niemożności takiej formalizacji (K_U07)

Zaliczenie na podstawie prac domowych i końcowego egzaminu ustnego.