1. SylabUZ
2. Faculty of Computer Science, Electrical Engineering and Automatics
3. winter term 2022/2023
4. Automatic Control and Robotics / Computer Control Systems - Second-cycle Erasmus programme
5. Event-driven systems

Generate PDF for this page

Event-driven systems - course description

Aim of the course

Get to know formal specification methods of event-driven systems.

Learn how to design and verify event-driven systems.

Prerequisites

Save changes

Finishing the course of "Discrete process control"

Scope

Informal introduction to event-driven systems.

Mathematical foundations. Elements of automata theory that are necessary for the formal specification of event-driven systems. A finite automaton as an event-driven system model. Deterministic and nondeterministic automata.

Introduction to temporal logic. Time structure - linear and branched time. Operators and formulas of temporal logic. Logic: LTL vs CTL. Intuitive examples of the specification of simple event systems in the language of temporal logic.

Reactive systems. Synchronous and asynchronous implementation of event systems.

Formal verification of the specification of event systems. System analysis by examining the specification set in the LTL and CTL logics. Safety and liveness properties. Counter-examples. Model checking methods. The use of a model checker tool (on the example of NuSMV/nuXmv).

Teaching methods

lecture: classic lecture & discussion

lab: exercises

Learning outcomes and methods of theirs verification

Outcome description	Outcome symbols	Methods of verification	The class form

Assignment conditions

lecture: passing the exam

lab: positive evaluation of finished exercises

final grade = lecture: 50% + lab: 50%

Recommended reading

1. Ch. Baier, J.-P. Katoen, Principles of Model Checking, MIT Press, 2008.
2. O. Grumberg, H. Veith (Eds.): 25 Years of Model Checking - History, Achievements, Perspectives. Lecture Notes in Computer Science 5000, Springer, 2008.
3. T.Kropf, Introduction to Formal Hardware Verification. Springer, Berlin, 1999
4. R. Cavada, A. Cimatti, G. Keighren, E. Olivetti, M. Pistore, M Roveri, NuSMV 2.5 Tutorial (http://nusmv.fbk.eu/NuSMV/tutorial/index.html)
5. C. Girault, R. Volk, Petri Nets for Systems Engineering. A Guide to Modeling, Verification and Applications, Springer Verlag, Berlin, 2003

Further reading

Notes

Modified by dr hab. inż. Wojciech Paszke, prof. UZ (last modification: 11-04-2022 09:05)