System Modeling and Analysis

Lecturer:

Stefan Ratschan (gar.)

Tutor:

Stefan Ratschan (gar.)

Supervisor:

Department of Digital Design

Synopsis:

Students are introduced to methods of hardware and software systems based on gradual refinement of the description. They understand importance of modeling at the system level, they learn to validate and verify the properties of modelled systems using formal methods and simulation experiments.

Requirements:

Advanced C++ programming,

Syllabus of lectures:

1. State description of the system, automata as models.

2. Extended finite state machine (FSM), cooperating FSMs.

3. Verification of the automaton model, SPIN.

4. Temporal logic as a behavioral model, derived languages.

5. Alternative models - Petri nets, process algebras, LOTOS.

6. Time properties of applications, the RM analysis.

7. Scheduling strategies, the RM and EDF scheduling.

8. Queueing system models, Markov automata.

9. M/M/1, M/D/1, M/M/n, and M/D/n systems, simulation.

10. Performance validation and predictability.

11. Performance optimization.

12. Functionality validation. Dynamic checking.

13. Formal verification and combined methods.

Syllabus of tutorials:

Study Objective:

Modern systems - networks or embedded systems - consist of many components working in parallel. The behavior and peformance of the system as a whole is difficult to determine analytically. Deployment of ill-designed or low-performance system leads to significant losses. Students learn to work with models based on stateful descriptions and temporal logic that allows to describe the behavior of the target system, verify its correctness, and avoid problems such as deadlocks. Students will get acquainted with models based on the principles of queuing theory that allow to estimate, or verify by simulation, the behavior of queuing systems under load.

Study materials:

1. Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P. ''Systems and Software Verification: Model-Checking Techniques and Tools''. Springer, 2001. ISBN 3540415238.

2. Holzmann, G. J. ''The SPIN Model Checker: Primer and Reference Manual''. Addison-Wesley Professional, 2003. ISBN 0321228626.

3. Kleinrock, L., Gail, R. ''Queueing Systems: Problems and Solutions''. Wiley-Interscience, 1996. ISBN 0471555681.

4. Roychoudhury, A. ''Embedded Systems and Software Validation''. Morgan Kaufmann, 2009. ISBN 0123742307.

Note:

Further information:

No time-table has been prepared for this course

The course is a part of the following study plans:

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