Modelowanie i Analiza Systemów Informatycznych (laboratoria)

dla studentów informatyki (1 rok, mgr.).
kod kursu: INEU00004L

Studenci modelują, symulują i weryfikują informacyjne i transportowe systemy, używając Sieci Petriego, logiki temporalnej i automatów czasowych.

Laboratoria z Sieci Petriego trwają środkowe 5 zajęć; laboratoria z Logiki Temporalnej i Automatów Czasowych trwają ostatnie 5 zajęć z Modelowania i Analizy Systemów Informatycznych.

Ćwiczenia z Logiki Temporalnej i Automatów Czasowych studenci mogą wykonywać w 2-osobowych zespołach.

Plan zajęć

Sieci Petriego

  1. część (zajęcia 6): Wprowadzenie do Sieci Petriego
    • Studenci budują i symulują proste zwykłe Sieci Petriego.
    • Sprawozdanie na: zajęcia 7
  2. część (zajęcia 7 – 8): Zwykłe Sieci Petriego
    • Studenci budują modele Sieci Petriego.
    • Sprawozdanie na: zajęcia 9
  3. część (zajęcia 9 – 10): Czasowe Sieci Petriego
    • Studenci budują modele Czasowych Sieci Petriego.
    • Sprawozdanie na: zajęcia 10

Narzędzie do Sieci Petriego: TAPAAL i Pipe.

Logika Temporalna i Automaty Czasowe

  1. część (zajęcia 11): Automaty Czasowe UPPAAL
    • Studenci uczą się używać narzędzie UPPAAL oraz modelują i symulują proste automaty czasowe.
    • Sprawozdanie na: zajęcia 12
  2. część (zajęcia 12 – 13): Modelowa Weryfikacja Systemów w UPPAAL
    • Studenci tworzą i interpretują formuły CTL oraz modelują i weryfikują systemy.
    • Sprawozdanie na: zajęcia 14
  3. część (zajęcia 14 – 15): Modelowa Weryfikacja Systemów w NuSMV
    • Studenci uczą się używać narzędzie NuSMV, tworzą i interpretują formuły LTL, CTL i RTCTL oraz modelują i weryfikują systemy.
    • Sprawozdanie na: 2 lutego

Narzędzia do automatów czasowych: UPPAAL i NuSMV.

Jak zainstalować NuSMV na Linuxie (Ubuntu)

Sprawozdania

Sprawozdania muszą być wydrukowane lub napisane na papierze. Proszę podać swoje imię, nazwisko i nr indeksu w lewym górnym rogu okładki. Proszę nie zszywać kartek, ale raczej użyć spinacza.

Sprawozdanie musi zawierać rezultaty ćwiczeń z instrukcji laboratoryjnej.

Proszę nie dodawać żadnej teorii czy innych rzeczy, o które nie prosi instrukcja laboratoryjna.

Poprawa sprawozdania, które zostało nisko ocenione, nie jest obowiązkowa. Jednakże jest możliwa w ciągu jednego tygodnia.

Oceny

Oceny cząstkowe i końcowe

Studenci otrzymają oceny za każdą ostateczną wersję sprawozdania. Są to oceny cząstkowe.

Oceną za Sieci Petriego jest średnia 3 ocen cząstkowych za sprawozdania z tego tematu. Oceną za Logikę Temporalną i Automaty Czasowe jest średnia 3 ocen cząstkowych za sprawozdania z tego tematu. Wszystkie te oceny, wraz z oceną za /pierwsze 5 laboratoriów/, te trzy oceny utworzą ocenę końcową.

 

Comments are closed.