Embedded systems: models and verification - NSWI136

• Title: Vestavěné systémy: modely a verifikace
• Guaranteed by: Department of Software Engineering (32-KSI)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2010
• Semester: winter
• E-Credits: 3
• Hours per week, examination: winter s.:2/0, Ex [HT]
• Capacity: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: cancelled
• Language: Czech
• Teaching methods: full-time
• Teaching methods: full-time
• Guarantor: doc. Ing. Stefan Ratschan, Ph.D.
• Class: Informatika Mgr. - volitelný
• Classification: Informatics > Software Engineering
• Pre-requisite : NSWI101

Annotation

English

Last update: T_KSI (25.03.2009)

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.

Czech

Last update: 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ů.

Literature

Last update: 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

Syllabus

English

Last update: T_KSI (25.03.2009)

• 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

Czech

Last update: 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)