System Modeling and Analysis

Lecturer:

Stefan Ratschan (gar.)

Tutor:

Stefan Ratschan (gar.)

Supervisor:

Department of Digital Design

Synopsis:

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 is the topic of this subject.

Requirements:

Syllabus of lectures:

1. Automata-based models

2. Temporal logic

3. Testing and bounded model checking

4. Bounded model checking and Boolean satisfiability

5. Unbounded model checking

6. Data structures for unbounded model checking

7. Petri nets

8. Timed automata

9. Modeling the physical environment

10. Simulation

11. Probabilistic models

Syllabus of tutorials:

Practical training of the lecture material.

Study Objective:

The student will have the ability to use and apply some of the most important formalisms for modeling complex systems. He/she will also be familiar with techniques for the automatic analysis of such models.

Study materials:

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.

Note:

Time-table for winter semester 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
Mon	roomT9:349 Ratschan S. 14:30–16:00 (lecture parallel1) Dejvice NBFIT místnost
Tue
Fri
Thu	roomT9:302 Ratschan S. 12:45–14:15 ODD WEEK (lecture parallel1 parallel nr.101) Dejvice NBFIT učebna roomT9:302 Ratschan S. 12:45–14:15 EVEN WEEK (lecture parallel1 parallel nr.102) Dejvice NBFIT učebna
Fri

Time-table for summer semester 2011/2012:

Time-table is not available yet

The course is a part of the following study plans:

• Design of Digital Systems, Version for Students who Enrolled in 2010, Presented in Czech (compulsory course of the specialization)
• Master Informatics, Version for Students who Enrolled in 2010, Presented in Czech (VO)
• Master Informatics, Presented in Czech, Version for Students who Enrolled in 2011 (VO)
• Design of Digital Systems, Presented in Czech, Version for Students who Enrolled in 2011 (compulsory course of the specialization)
• Master Informatics, Presented in Czech, Version for Students who Enrolled in 2012 (VO)