Rankiem 4 czerwca 1996 rakieta Arianne-5 wybuchła w powietrzu, 36 sekund po starcie z kosmodromu w Gujanie Francuskiej. Przyczyną był nieobsłużony wyjątek, spowodowany nieudaną konwersją z 64-bitowej liczby zmiennopozycyjnej na 16-bitową liczbę całkowitą. Awarii spowodowanych wadliwym działaniem oprogramowania było więcej. Ulegały im m.in. lądownik marsjański Mars Pathfinder, samolot Airbus czy centrala telefoniczna AT&T. Niektóre z nich pociągnęły ofiary, np. awaria urządzenia Therac-25 stosowanego w radioterapii.

Wykład poświęcony jest metodom weryfikacji pozwalającym na zwiększenie niezawodności systemów komputerowych. Ograniczymy się do tzw. metod formalnych, tzn. opartych na ścisłych podstawach matematycznych, i na ogół w duźym stopniu automatycznych. Omówimy trzy najważniejsze grupy podejść: weryfikacja modelowa (ang. model-checking), analiza statyczna (ang. static analysis) i dowodzenie poprawności programów. Pierwsza z nich odniosła już sukces przemysłowy w weryfikacji układów sprzętowych; połączenie dwóch pozostałych pozwala odnaleźć rozsądny kompromis pomiędzy siłą metody a jej efektywnością, i wydaje się być najlepsze w weryfikacji programów. W ramach wykładu omówione zostaną podstawy teoretyczne i algorytmy. W czasie laboratorium studenci zapoznają się z kilkoma narzędziami. Wykonają też własne projekty, co pozwoli lepiej zrozumieć treść wykładu.

Zagadnienia:

  • wprowadzenie do weryfikacji formalnej
  • logiki temporalne: LTL, CTL, CTL*
  • omega-automaty, weryfikacja modelowa dla LTL
  • redukcja częściowo-porządkowa
  • BDD, weryfikacja symboliczna dla CTL
  • weryfikacja ograniczona dla LTL przez sprowadzenie do SAT
  • metody abstrakcji
  • statyczna analiza programów
  • interpretacja abstrakcyjna
  • specyfikacja i dowodzenie poprawności programów
  • automaty czasowe (opcjonalnie)
  • weryfikacja probabilistyczna (opcjonalnie)