Analýza systémů založená na modelech - informace pro studenty

Přednášky

Materiály použité na přednáškách:

1: Úvod do model checkingu, přechodové systémy

Materiály z minulých z loňského roku jsou dostupné zde.

Učebnice a materiály

Milan Češka a kolektiv: Studijní opora Petriho sítě, 2006, dostupné: odkaz
Javier Esparsa: Petri Nets Lecture Notes, 2022, dostupné: odkaz
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, Dostupné online
UPPAAL 4.0: Small Tutorial online
Stochastic Model Checking (mimo jiné analýza CTMC) online
Automated Verification Techniques for Probabilistic Systems (mimo jiné analýza MDP) online

Nástroje

Většina nástrojů používaná na cvičeních je k dispozici na školních počítačích s linuxem (včetně merlina) ve složce: /usr/local/groups/verifikace/MBA-tools-linux

CeSIM (C/E systémy): dostupné zde (možnost použít pod Wine)
Netlab (P/T Petriho sítě): binárka pro Windows (možno použít i pod Wine): zde, Zdrojové kódy: zde.
Uppaal (Časované automaty): dostupné na http://www.uppaal.org/
PRISM (Analýza pravděpodobnostních modelů): dostupné na https://www.prismmodelchecker.org/