Modelování a analýza systémů

Přednášející:

Stefan Ratschan (gar.)

Cvičící:

Stefan Ratschan (gar.)

Předmět zajišťuje:

katedra číslicového návrhu

Anotace:

Lidstvo dnes má schopnost konstruovat systémy neuvěřitelné složitosti (např. vlaky, mikroprocesory, letadla). Náklady pro zvládání této složitosti a pro zajištění správného fungování jsou ale stále kritičtější. Důležitá metoda pro zvládání tuto složitost je používání modelů, které popisuje výhradně tyto aspekty daného sytému, které jsou nutné pro daný úkol. Další důležitý prvek je automatizace analýzy takovýchto modelů. Metody modelování a analýzy složitých systémů je obsahem tohoto předmětu.

Požadavky:

Osnova přednášek:

1. Automatové modely

2. Temporální logika

3. Testování, omezené ověřování modelů

4. Omezené ověřování modelů a Booleovská splnitelnost

5. Neomezené ověřování modelů

6. Datové struktury pro ověřování modelů

7. Petriho sítě

8. Časované automaty

9. Modelování fyzikálního okolí

10. Simulace

11. Probabilistické modely

Osnova cvičení:

Cvičení materiálu z přednášky.

Cíle studia:

Studenti budou mít schopnost používat několik důležitých formalizmů pro modelování složitých systémů. Budou znát techniky pro automatickou analýzu takových modelů.

Studijní materiály:

Edward A. Lee and Sanjit A. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, http://LeeSeshia.org, ISBN 978-0-557-70857-4, 2011.

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999.

Poznámka:

Rozsah=prednasky+proseminare+cviceni2p+1c, Prednasejici: doc. Ing. Jan Janeček CSc.

Rozvrh na zimní semestr 2011/2012:

	06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Po	místnost T9:349 Ratschan S. 14:30–16:00 (přednášková par. 1) Dejvice NBFIT místnost
Út
St
Čt	místnost T9:302 Ratschan S. 12:45–14:15 LICHÝ TÝDEN (přednášková par. 1 paralelka 101) Dejvice NBFIT učebna místnost T9:302 Ratschan S. 12:45–14:15 SUDÝ TÝDEN (přednášková par. 1 paralelka 102) Dejvice NBFIT učebna
Pá

Rozvrh na letní semestr 2011/2012:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Projektování číslicových systémů - verze pro ty, kteří se zapsali v roce 2010 (povinný předmět oboru)
• Společný plán před přiřazením do oboru, verze pro ty, kteří se zapsali v roce 2010 (VO)
• Společný plán před přiřazením do oboru, verze pro ty, kteří se zapsali v roce 2011 (VO)
• Projektování číslicových systémů - verze pro ty, kteří se zapsali v roce 2011 (povinný předmět oboru)
• Společný plán před přiřazením do oboru, verze pro ty, kteří se zapsali v roce 2012 (VO)