Oferta dydaktyczna Instytutu Informatyki

Poniższa lista przedstawia przedmioty, które są uczone w Instytucie Informatyki, niektóre z nich co roku, niektóre z mniejszą częstotliwością Każdy student Instytutu Informatyki studiuje wg indywidualnego toku studiów, wybierając (zgodnie z pewnymi zasadami) z tej listy swoje przedmioty.

Jeżeli zastanawiasz się nad studiami u nas, jeżeli chcesz wiedzieć, czy na Uniwersytecie można zostać inżynierem, jeżeli interesuje Cię 1000 zł stypendium miesięcznie - zapraszamy na naszą stronę główną

Modelowanie i weryfikacja systemów reaktywnych

Nazwa angielska (title in English): Verification of reactive systems
Prowadzący (lecturer): Piotr Witkowski
Liczba punktów (ECTS): 3
Liczba punktów 2007 (ECTS since 2007): 5
Rodzaj (type): kurs
Rodzaj od 2007 (type since 2007): kurs
Liczba godzin (hours in semester):
wykład:30
ćwiczenia+pracownia:30
Egzamin (exam): nie
Możliwe zajęcia w języku angielskim (can be taught in English): nie
Przedmiot zostal uaktualniony na biezacy rok (updated): tak
Semestr (semester): letni

Wymagania (prerequisites)

Opis (description)

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. Przez większą część semestru studenci będą modelować i weryfikować fragmenty wybranych systemów reaktywnych. Błędy fazy projektowania i błędy oprogramowania doprowadziły w przeszłości do wielu kosztownych porażek( np. THERAC-25, Arianne-5). Pokażemy, że weryfikacja modelowa pozwoliłaby ich, w znacznej mierze, uniknąć.

Wykład zostanie przeprowadzony w sposób przystępny dla studentów młodszych lat.

Literatura (references)

Jeżeli jesteś zainteresowany studiowaniem w naszym instytucie, zapraszamy na stronę poświęconą tegorocznej rekrutacji.

Nazwa użytkownika (user name):
Hasło (password):