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

Anotace

čeština

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ů.

Poslední úprava: T_KSI (25.03.2009)

angličtina

Nowadays, by far the most microchips do not occur in desktop computers, but as embedded computing devices in cars, trains, robots, and the usual household equipment. However, the classical engineering approaches use continuous mathematical models to describe technical systems, while the computing field employs discrete models. In the lecture we will discuss formalisms bridging this gap and algorithms and software tools for the verification of the resulting models.

Poslední úprava: T_KSI (25.03.2009)

Literatura

• 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

Poslední úprava: T_KSI (25.03.2009)

Sylabus

čeština

• 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)

Poslední úprava: T_KSI (25.03.2009)

angličtina

• Examples of embedded systems

• Software tools for modelling embedded systems (SCILAB/SCICOS)

• Basics of continuous dynamical systems and control theory

• Formalisms with simple continuous dynamics: timed automata (+ applications)

• Formalisms with more general continuous dynamics (switched systems, hybrid automata, ...)

• Simulation: algorithms and tools

• Zeno behavior and similar phenomena

• Decidability, quasi-decidability, robustness

• Safety verification: algorithms and tools

• Verification of more complicated properties

• Model predictive control

Poslední úprava: T_KSI (25.03.2009)