System Modeling and Analysis

Předmět není vypsán Nerozvrhuje se

Kód	Zakončení	Kredity	Rozsah	Jazyk výuky
MIE-MAS	Z,ZK	4	2+1

Přednášející:

Stefan Ratschan (gar.)

Cvičící:

Stefan Ratschan (gar.)

Předmět zajišťuje:

katedra číslicového návrhu

Anotace:

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.

Požadavky:

Advanced C++ programming,

Osnova přednášek:

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.

Osnova cvičení:

Cíle studia:

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.

Studijní materiály:

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.

Poznámka:

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

Další informace:

Pro tento předmět se rozvrh nepřipravuje

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