Moduł oferowany także w ramach programów studiów:
Informacje ogólne:
Nazwa:
Metody formalne
Tok studiów:
2019/2020
Kod:
EINF-2-104-GK-s
Wydział:
Elektrotechniki, Automatyki, Informatyki i Inżynierii Biomedycznej
Poziom studiów:
Studia II stopnia
Specjalność:
Grafika komputerowa
Kierunek:
Informatyka
Semestr:
1
Profil:
Ogólnoakademicki (A)
Język wykładowy:
Polski
Forma studiów:
Stacjonarne
Strona www:
 
Prowadzący moduł:
Szmuc Tomasz (tsz@agh.edu.pl)
Treści programowe zapewniające uzyskanie efektów uczenia się dla modułu zajęć

Celem modułu jest przekazanie wiedzy i umiejętności związanych z modelowaniem
i weryfikacją oprogramowania z zastosowaniem metod formalnych: sieci Petriego, algebry procesów, logiki temporalne.

Opis efektów uczenia się dla modułu zajęć
Kod MEU Student, który zaliczył moduł zajęć zna i rozumie/potrafi/jest gotów do Powiązania z KEU Sposób weryfikacji i oceny efektów uczenia się osiągniętych przez studenta w ramach poszczególnych form zajęć i dla całego modułu zajęć
Wiedza: zna i rozumie
M_W001 Zna podstawowe języki formalnego modelowania systemów informatycznych INF2A_W04 Egzamin,
Kolokwium
M_W002 Ma podstawową wiedzę w zakresie metod formalnej weryfikacji systemów informatycznych INF2A_W04 Egzamin,
Kolokwium
M_W003 Zna systemy wspomagające modelowanie i weryfikację z zastosowaniem metod formalnych INF2A_W04 Egzamin,
Kolokwium
Umiejętności: potrafi
M_U001 Potrafi zastosować metody formalne w analizie i projektowaniu systemów informatycznych INF2A_U05 Egzamin,
Kolokwium
M_U002 Potrafi korzystać z systemów wspomagających formalne modelowanie i weryfikację INF2A_U05 Egzamin,
Kolokwium
Kompetencje społeczne: jest gotów do
M_K001 rozumie potrzebę formułowania i przekazywania społeczeństwu informacji i  opinii dotyczących roli metod formalnych i ich wpływu na jakość tworzonego oprogramowania INF2A_K02 Egzamin,
Kolokwium
Liczba godzin zajęć w ramach poszczególnych form zajęć:
SUMA (godz.)
Wykład
Ćwicz. aud
Ćwicz. lab
Ćw. proj.
Konw.
Zaj. sem.
Zaj. prakt
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
56 28 0 28 0 0 0 0 0 0 0 0
Matryca kierunkowych efektów uczenia się w odniesieniu do form zajęć i sposobu zaliczenia, które pozwalają na ich uzyskanie
Kod MEU Student, który zaliczył moduł zajęć zna i rozumie/potrafi/jest gotów do Forma zajęć dydaktycznych
Wykład
Ćwicz. aud
Ćwicz. lab
Ćw. proj.
Konw.
Zaj. sem.
Zaj. prakt
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
Wiedza
M_W001 Zna podstawowe języki formalnego modelowania systemów informatycznych + - + - - - - - - - -
M_W002 Ma podstawową wiedzę w zakresie metod formalnej weryfikacji systemów informatycznych + - + - - - - - - - -
M_W003 Zna systemy wspomagające modelowanie i weryfikację z zastosowaniem metod formalnych + - + - - - - - - - -
Umiejętności
M_U001 Potrafi zastosować metody formalne w analizie i projektowaniu systemów informatycznych + - + - - - - - - - -
M_U002 Potrafi korzystać z systemów wspomagających formalne modelowanie i weryfikację + - + - - - - - - - -
Kompetencje społeczne
M_K001 rozumie potrzebę formułowania i przekazywania społeczeństwu informacji i  opinii dotyczących roli metod formalnych i ich wpływu na jakość tworzonego oprogramowania + - + - - - - - - - -
Nakład pracy studenta (bilans punktów ECTS)
Forma aktywności studenta Obciążenie studenta
Sumaryczne obciążenie pracą studenta 86 godz
Punkty ECTS za moduł 3 ECTS
Udział w zajęciach dydaktycznych/praktyka 56 godz
przygotowanie projektu, prezentacji, pracy pisemnej, sprawozdania 10 godz
Samodzielne studiowanie tematyki zajęć 20 godz
Szczegółowe treści kształcenia w ramach poszczególnych form zajęć (szczegółowy program wykładów i pozostałych zajęć)
Wykład (28h):
Tematyka wykładów

1. Metody formalne w informatyce (2 godz)
Zagadnienia modelowania formalnego. Klasy metod formalnych i ich zastosowania
2. Metody formalne w inżynierii oprogramowania (2 godz)
Rola metod formalnych.
Poprawność weryfikacja, walidacja. Normy
3. Sieci Petriego (10 godz)
Sieci miejsc i przejść. Definicja, własności, metody analizy.
Sieci kolorowane.
Hierarchiczne sieci Petriego
Modelowanie z zastosowaniem sieci Petriego
4. Algebry procesów (10 godz)
Podstawowe pojęcia algebry CCS (Calculus of Communicating Systems)
Relacje równoważności i ich zastosowanie
Język LOTOS
Modelowanie z zastosowaniem LOTOS
5. Logika temporalna (6 godz)
Logika modalna i logiki temporalne
Operatory logiki temporalnej
Logika czasu liniowego (LTL) i rozgałęzionego (CTL)
Modelowanie i Analiza własności

Ćwiczenia laboratoryjne (28h):
Tematyka ćwiczeń laboratoryjnych

1. Wprowadzenie do systemu modelowania sieci
2. Modelowanie prostych przykładów
3. Wprowadzenie do systemu CADP
4. Modelowanie przykładów
5. Przykłady modelowania i weryfikacji z zastosowaniem logiki temporalnej

Pozostałe informacje
Metody i techniki kształcenia:
  • Wykład: Treści prezentowane na wykładzie są przekazywane w formie prezentacji multimedialnej w połączeniu z klasycznym wykładem tablicowym wzbogaconymi o pokazy odnoszące się do prezentowanych zagadnień.
  • Ćwiczenia laboratoryjne: W trakcie zajęć laboratoryjnych studenci samodzielnie rozwiązują zadany problem praktyczny, dobierając odpowiednie narzędzia. Prowadzący stymuluje grupę do refleksji nad problemem, tak by otrzymane wyniki miały wysoką wartość merytoryczną.
Warunki i sposób zaliczenia poszczególnych form zajęć, w tym zasady zaliczeń poprawkowych, a także warunki dopuszczenia do egzaminu:

Zasady udziału w zajęciach:
  • Wykład:
    – Obecność obowiązkowa: Nie
    – Zasady udziału w zajęciach: Studenci uczestniczą w zajęciach poznając kolejne treści nauczania zgodnie z syllabusem przedmiotu. Studenci winni na bieżąco zadawać pytania i wyjaśniać wątpliwości. Rejestracja audiowizualna wykładu wymaga zgody prowadzącego.
  • Ćwiczenia laboratoryjne:
    – Obecność obowiązkowa: Tak
    – Zasady udziału w zajęciach: Studenci wykonują ćwiczenia laboratoryjne zgodnie z materiałami udostępnionymi przez prowadzącego. Student jest zobowiązany do przygotowania się w przedmiocie wykonywanego ćwiczenia, co może zostać zweryfikowane kolokwium w formie ustnej lub pisemnej. Zaliczenie zajęć odbywa się na podstawie zaprezentowania rozwiązania postawionego problemu. Zaliczenie modułu jest możliwe po zaliczeniu wszystkich zajęć laboratoryjnych.
Sposób obliczania oceny końcowej:

Ocena końcowa wyznaczana jest jako średnia ocen z zaliczenia i egzaminu. Jeżeli zaliczenie nie zostało uzyskane w pierwszym terminie lub egzamin nie został zdany w pierwszym terminie, to przy wyznaczaniu oceny końcowej bierze się pod uwagę również oceny niedostateczne z terminów poprzedzających uzyskanie zaliczenia lub zdanie egzaminu. W takim przypadku wyznaczana jest średnia z więcej niż dwóch ocen.

Sposób i tryb wyrównywania zaległości powstałych wskutek nieobecności studenta na zajęciach:

Wymagania wstępne i dodatkowe, z uwzględnieniem sekwencyjności modułów :

Znajomość elementów matematyki dyskretnej: algebra relacji, teoria grafów, podstawy logiki matematycznej
Znajomość teorii automatów

Zalecana literatura i pomoce naukowe:

1. Huzar Z.: LOTOS – język formalnych specyfikacji systemów informatycznych. Oficyna Wydawnicza Polit. Wroc., 2007
2. Jensen K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, Vol. I-III, Springer Verlag, 1995/96
3. Szmuc T.: Inżynieria Oprogramowania Systemów Czasu Rzeczywistego, Wydawnictwa Naukowo-Dydaktyczne AGH 2001
4. Szpyrka M.: Sieci Petriego w modelowaniu i analizie systemów współbieżnych. WNT, Warszawa, 2008
5. Szmuc T., Szpyrka M.: Metody formalne w inżynierii o-programowania systemów czasu rzeczywistego. WNT, 2010

Publikacje naukowe osób prowadzących zajęcia związane z tematyką modułu:

Szmuc T.: Inżynieria Oprogramowania Systemów Czasu Rzeczywistego, Wydawnictwa Naukowo-Dydaktyczne AGH 2001
Szmuc T., Szpyrka M.: Metody formalne w inżynierii o-programowania systemów czasu rzeczywistego. WNT, 2010

Informacje dodatkowe:

Brak