Seminář UPSY - Strnadel J.: Modelování a analýza (real-time) systémů

Zájemcům představím základní aspekty mnou používaných prostředků modelováni a analýzy (real-time) systémů. Výpočetní model těchto prostředků vychází z časovaných automatů (timed automata, TA) a jejich mnohých rozšíření (probabilistic TA, stochastic TA, priced TA, stopwatch TA, ...). Konkrétní systém je modelován jako síť potencionálně vzájemně komunikujících TA, požadované vlastnosti systému jsou vyjádřeny v rozšířeném jazyku odnože CTL logiky. Analýza systému je realizována metodou ověřování modelu (model checking, MC), který je klasicky symbolicky, tj. 100% garantující ne/splnění dané vlastnosti v celém stavovém prostoru možných chování systému; zejména u komplexních systémů však může být výsledek takového ověřování "v nedohlednu". Alternativou ke klasickému MC je např., na simulaci založený, statisticky model checking, u kterého se spokojíme s určitou, předem danou, chybou/nepřesností při ověřovaní modelu. Nad výše zmíněnými prostředky lze využít další nadstavby jako např. syntézu, učení, optimalizaci či vyhodnocení strategií řízení modelovaných systémů. Vzhledem k náročnosti a komplexnosti problematiky a snaze/výzvě vše vměstnat cca do 50 minut se vynasnažím zásadní představit formou předem připravených ilustrativních demo ukázek v prostředí frameworku UPPAAL.