1. SylabUZ
2. Faculty of Computer Science, Electrical Engineering and Automatics
3. winter term 2018/2019
4. WIEiA - oferta ERASMUS / Automatic Control and Robotics - Second-cycle Erasmus programme
5. Event-driven systems

Generate PDF for this page

Event-driven systems - course description

Aim of the course

• To provide knowledge on the ways and methods of formal specification of the event-driven systems
• To maintain the theoretcal basis necessary for understanging the ways of design and verification odf the event-driven systems

Prerequisites

Save changes

Discrete process control

Scope

Informal introduction to the event-driven systems.

Mathematical foundations. Elements of the automata theory necessary for formal specification of an event-driven systems. Finite Stste Machine as a model of an event-driven systems. Deterministic and undeterministic automata.

Introduction to the temporal logic. Structore of the time, linear and branchung time. Operators and expressions of the temporal logic. Logic LTL, CTL, CTL*. Intuitive examples of specification of the simple event-driven systems using the temporal logic.

Reactive event-driven systems. General concept of HCFSM. Synchronous and asynchronous implementation of the event-driven systems.

Formal verification of the event-driven systems at the level of specification. System analysis by mean of studying of the specification which provided using LTL or CTL. "Safeness" and "liveness" propertries. "Liveness" and "safeness" properties. Counter-examples. Methods of model checking. Using a model checker (NuSMV is used as an example of such tool.)

 

Teaching methods

Lecture: conventional lecture
Laboratory: laboratory exercises

Learning outcomes and methods of theirs verification

Outcome description	Outcome symbols	Methods of verification	The class form

Assignment conditions

Lecture: The condition of pass is to obtain a positive assessment from the written examination.
Laboratory: a conditional of pass is to obtain positive grades from all laboratory exercises that are expected to be performed within the laboratory program.

Components of the final grade: lecture: 50% + laboratory: 50%

Recommended reading

1. Baier Ch., Katoen J.-P.: Principles of Model Checking, MIT Press, 2008.
2. Cavada R., Cimatti A., Keighren G., Olivetti E., Pistore M., Roveri M.: NuSMV 2.5 Tutorial (http://nusmv.fbk.eu/NuSMV/tutorial/index.html).
3. Clarke E. M., Jr., Grumnerg O., Peled D. A.: Model Checking, MIT Press, 1999.
4. Emerson E. A., Temporal and modal logic, Handbook of Theoretical Computer Science, Chapter 16, MIT Press, 1990.
5. Grobelna I.: Model Verification with NuSMV, Oficyna Wydawnicza Uniwersytetu Zielonogórskiego, Zielona Góra, 2011. (in Polish).
6. Pecol J.: Embedded Systems. A Contemporary Design Tool, Willey, 2008.

Further reading

1. Girault G., Volk R.: Petri Nets for Systems Engineering. A Guide to Modeling, Verification and Applications, Springer Verlag, Berlin, 2003.
2. Grumberg O., Veith H. (Eds.): 25 Years of Model Checking - History, Achievements, Perspectives. Lecture Notes in Computer Science 5000, Springer, 2008.
3. Kropf T., Introduction to Formal Hardware Verification, Springer, Berlin, 1999.
4. Øhrstrøm P., Hasle P. F. V.: Temporal logic: from ancient ideas to artificial intelligence, Springer, 1995

Notes

Modified by dr hab. inż. Wojciech Paszke, prof. UZ (last modification: 30-04-2020 10:55)