Wykład prowadzony wspólnie z Witoldem Charatonikiem.
Jednym z etapów projektowania złożonych systemów (nie tylko informatycznych!)
jest opracowanie modelu zagadnienia. Taki model definiuje aktorów, czyli byty
wykonujące zadane programy (najczęściej współbieżnie) i komunikujące się
ustalonymi kanałami. Metody formalne pozwalają badać modele, dowodzić pewnych
ich własności lub wyjaśniać, dlaczego dana własność nie zachodzi.
Nas będzie interesować weryfikowanie modeli systemów reaktywnych, silnie
zależnych od czynników zewnętrznych. Takimi systemami są np.zautomatyzowane
linie produkcyjne, komputery pokładowe samochodów - systemy ABS czy
dynamicznego ustalania składu mieszanki paliwowej, systemy utrzymania ruchu
kolejowego, awionika. W pierwszej części kursu przedstawimy pokrótce logiki
temporalne(LTL, CTL), następnie omówimy wybrane narzędzia weryfikacji
modelowej (np. SPiN, nuSMV, Vereofy) i metody modelowania.
