PředmětyPředměty(verze: 945)
Předmět, akademický rok 2023/2024
   Přihlásit přes CAS
Vestavěné systémy: modely a verifikace - NSWI136
Anglický název: Embedded systems: models and verification
Zajišťuje: Katedra softwarového inženýrství (32-KSI)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2010
Semestr: zimní
E-Kredity: 3
Rozsah, examinace: zimní s.:2/0, Zk [HT]
Počet míst: neomezen
Minimální obsazenost: neomezen
4EU+: ne
Virtuální mobilita / počet míst pro virtuální mobilitu: ne
Stav předmětu: zrušen
Jazyk výuky: čeština
Způsob výuky: prezenční
Způsob výuky: prezenční
Garant: doc. Ing. Stefan Ratschan, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Softwarové inženýrství
Prerekvizity : NSWI101
Výsledky anket   Termíny zkoušek   Rozvrh   Nástěnka   
Anotace -
Poslední úprava: T_KSI (25.03.2009)
V dnešní době se zdaleka největší počet mikročipů nenachází v osobních počítačích, ale ve formě vestavěných systémů v autech, vlacích, robotech a domácích spotřebičích. Klasické inženýrské přístupy používají spojité matematické modely pro popisování technických systémů, zatímco informatika používá diskrétní modely. V přednášce budeme diskutovat formalismy překonávající tento protiklad a algoritmy a softwarové nástroje pro verifikaci vyplývajících modelů.
Literatura
Poslední úprava: T_KSI (25.03.2009)
  • A. J. van der Schaft and J. M. Schumacher: An Introduction to Hybrid Dynamical Systems, Springer, 2000
  • Proceedings of HSCC conference series (Hybrid Systems: Computation and Control)
  • recent research articles

Sylabus -
Poslední úprava: T_KSI (25.03.2009)
  • Příklady vestavěných systémů
  • Softwarové nástroje pro modelování vestavěných systémů (SCILAB/SCICOS)
  • Základy spojitých dynamických systémů a teorie řízení
  • Formalismy s jednoduchou spojitou dynamikou (timed automata) a jejich aplikace
  • Formalismy se složitou spojitou dynamikou (switched systems, hybrid automata)
  • Simulace: algoritmy a nástroje
  • Zeno a podobné fenomény
  • Rozhodnutelnost, kvazi-rozhodnutelnost, robustnost
  • Verifikace bezpečnosti: algoritmy a nástroje
  • Verifikace složitějších vlastností
  • Prediktivní řízení s modelem (model predictive control)

 
Univerzita Karlova | Informační systém UK