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:

  • introduction to formal verification
  • temporal logics: LTL, CTL, CTL*
  • omega-automata, LTL model-checking
  • partial-order reductions
  • BDD, symbolic CTL model-checking
  • bounded LTL model checking by reduction to SAT
  • abstraction methods
  • static program analysis
  • abstract interpretation
  • requirements specification and correctness proofs
  • timed automata (optional)
  • probabilistic model-checking (optional)