Modelowanie i Analiza Systemów Informatycznych (laboratoria)

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

Laboratoria z Modelowania i Analizy Systemów Informatycznych to: modelowanie, symulowanie i weryfikowanie systemów komunikacyjnych i transportowych, używając sieci Petriego, logiki temporalnej i automatów czasowych.

Kurs dzieli się na 3 5-zajęciowe części:

  1. Języki dziedzinowe (to prowadzi ktoś inny).
  2. Sieci Petriego.
  3. Logika Temporalna i Automaty Czasowe.

Zadania z 2. i 3. części wykonywane są przez studentów 2-osobowo.

Plan zajęć

Sieci Petriego

  • laboratoria 6 (zadania): Konstrukcja i analiza behawioralna sieci Petriego. Oddanie sprawozdania: laboratorium 7.
  • laboratoria 7 (zadania): Konstrukcja sieci Petriego z łukami hamującymi (cz. 1). Oddanie sprawozdania: laboratorium 8.
  • laboratoria 8 (zadania): Konstrukcja sieci Petriego z łukami hamującymi (cz. 2). Oddanie sprawozdania: laboratorium 9.
  • laboratoria 9 (zadania): Konstrukcja sieci Petriego o specjalnych cechach. Oddanie sprawozdania: laboratorium 10.
  • laboratoria 10 (zadania): Konstrukcja sieci Petriego z łukami czasowymi. Oddanie sprawozdania: laboratorium 11.

Logika Temporalna i Automaty Czasowe

  • laboratoria 11 (zadania): Konstrukcja prostych automatów UPPAAL. Oddanie sprawozdania: laboratorium 12.
  • laboratoria 12 (zadania): Konstrukcja i weryfikacja zsynchronizowanych czasowych automatów UPPAAL (cz. 1). Oddanie sprawozdania: laboratorium 13.
  • laboratoria 13 (zadania): Konstrukcja i weryfikacja zsynchronizowanych czasowych automatów UPPAAL (cz. 2). Oddanie sprawozdania: laboratorium 14.
  • laboratoria 14 (zadania): Konstrukcja i weryfikacja zsynchronizowanych automatów NuSMV. Oddanie sprawozdania: laboratorium 15.
  • laboratoria 15 (zadania): Konstrukcja i weryfikacja automatów NuSMV do analizy programu. Oddanie sprawozdania: 18 czerwca.

Jak zainstalować i używać NuSMV na Linuksie (Ubuntu)

Narzędzia

  • TAPAAL – dla normalnych i czasowych sieci PetriegoNets,
  • Pipe –dla normalnych i czasowych sieci PetriegoNets,
  • UPPAAL,
  • NuSMV.

Przydatne strony

Sprawozdania

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

Sprawozdanie musi zawierać wyniki wszystkich zadań podanych w instrukcji laboratoryjnej.

Poprawa sprawozdania, które zostało nisko ocenione, nie jest obowiązkowa, ale 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. Ocena cząstkowa zależy od punktów uzyskanych za zadania (można dostać do 10 pkt. za każde laboratorium): ocena = punkty/2.

Końcowa ocena za 2. część to średnia ocen za zadania z tej części.

Końcowa ocena za 3. część to średnia ocen za zadania z tej części.

Końcowa ocena to średnia końcowych ocen za wszystkie trzy części.

Comments are closed.