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ą. Podobnych, choć mniej wybuchowych, awarii było więcej: Mars Pathfinder, Airbus, ....
Wykład poświęcony jest weryfikacji modelowej (ang. model-checking), jednej z metod pozwalających na zmniejszenie liczby błędów w oprogramowaniu. Materiał obejmuje najważniejsze wyniki, którym metoda ta zawdzięcza swój sukces przemysłowy. 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 modelowej (ang. model-checking)
- LTL (ang. Linear Time Logic)
- omega-automaty, weryfikacja modelowa dla LTL
- redukcje częściowo-porządkowe
- CTL (ang. Computational Tree Logic)
- weryfikacja symboliczna dla CTL
- weryfikacja ograniczona
- metody abstrakcji
- automaty czasowe (ang. timed automata)
- weryfikacja probabilistyczna