Předmět je základní jednotka výuky, jejímž prostřednictvím si student osvojí ucelenou část souboru znalostí a dovedností, potřebnou pro zvládnutí studijního oboru/specializace. Za věcný obsah předmětu zodpovídá garant předmětu. Časovou náročnost předmětu zhruba vyjadřuje atribut předmětu rozsah kontaktní výuky. Například rozsah = 2+2  značí, že předmět bude mít týdně dvě hodiny přednášek a dvě hodiny cvičení týdně. Na závěr semestru musí vyučující provést vyhodnocení, nakolik si ten který student osvojil poznatky a dovednosti, kterých měl během výuky nabýt. Jakým způsobem toto hodnocení vyučující provedou určuje atribut způsob zakončení. U předmětu lze definovat, že předmět je zakončen pouze zápočtem(Z), klasifikovaným zápočtem(KZ), pouze zkouškou(ZK), nebo zápočtem a zkouškou(Z,ZK). Náročnost úspěšného absolvování předmětu je vyjádřena ECTS kreditními body. Výuka předmětu probíhá během semestru. Opakovaně se předmět vyučuje vždy v zimním(Z), nebo v letním(L) semestru každého akademického roku. Výjimečně může předmět být nabízen studentům v obou semestrech(Z,L). Za organizační zajištění výuky zodpovídá přiřazená katedra, která zejména vytvoří časový rozvrh předmětu a zajistí pro předmět vyučující. Někteří přednáší a zkouší, jiní vedou cvičení a udělují zápočty.
Obsahová náplň a další organizační informace, týkající se předmětu je popsána pomocí různých popisných textů(anotace, týdenní osnova, literatura, apod.)
$DODATEK_POPIS

Anotace:
Today, humankind has the ability to develop systems of incredible complexity (e.g., trains, microprocessors, airplanes, nuclear power plants). However, the costs of managing this complexity and of ensuring the correct behavior of a given system have become critical. A key technique for mastering this complexity is the usage of models that describe only those aspects of the systems that are important for the task at hand, and automated tools for analyzing those models. This subject will present theory and algorithms that form the basis for the modeling and analysis of complex systems.

Osnovy přednášek:

1.		System theory introduction.
2.		Logical basics.
3.		Systems and automata.
4.		Interacting system components.
5.		Temporal logics.
6.		Testing and bounded model checking.
7.		Boolean satisfiability (SAT).
8.		Unbounded model checking.
9.		Petri nets.
10.		Timed automata.
11.		Modeling the physical environment.
12.		Probabilistic models.
13.		Simulation and control of system models.

Osnovy cvičení:
Improving the understanding of the subject by solving example problems using pen and paper.

Literatura:

1.

Lee, E. A. - Seshia, S. A. : Introduction to Embedded Systems, A Cyber-Physical Systems Approach (2nd

Edition). MIT Press, 2017. ISBN 978-0-262-53381-2.

2.		Clarke, E. M. - Henzinger, Th.A. - Veith, H. - Bloem, R. (Eds.) : Handbook of Model Checking. Springer,
2018.		ISBN 978-3-319-10574-1.
3.		Alur, R. : Principles of Cyber-Physical Systems. MIT Press, 2015. ISBN 978-0-262-02911-7.

Požadavky:
None.

Předmět je ekvivalentní s MI-TES // Informace o předmětu a výukové materiály naleznete na https://moodle-vyuka.cvut.cz/course/view.php?id=2215

Předmět je zahrnut do těchto studijních plánů:

Plán Obor Role Dop. semestr NIE-SI.21 Software Engineering 2021 V 1 NIE-NPVS.21 Design and Programming of Embedded Systems 2021 PS 1 NIE-PB.21 Computer Security 2021 V 1 NIE-TI.21 Computer Science 2021 VO 1 NIE-PSS.21 Computer Systems and Networks 2021 V 1