Event-driven systems - opis przedmiotu

Informacje ogólne

Nazwa przedmiotu	Event-driven systems
Kod przedmiotu	11.9-WE-AutD-E-dS-Er
Wydział	Wydział Informatyki, Elektrotechniki i Automatyki
Kierunek	Automatyka i robotyka / Komputerowe Systemy Automatyki
Profil	ogólnoakademicki
Rodzaj studiów	Program Erasmus drugiego stopnia
Semestr rozpoczęcia	semestr zimowy 2022/2023

Informacje o przedmiocie

Semestr	1
Liczba punktów ECTS do zdobycia	3
Typ przedmiotu	obowiązkowy
Język nauczania	angielski
Sylabus opracował	dr inż. Iwona Grobelna

Formy zajęć

Forma zajęć	Liczba godzin w semestrze (stacjonarne)	Liczba godzin w tygodniu (stacjonarne)	Liczba godzin w semestrze (niestacjonarne)	Liczba godzin w tygodniu (niestacjonarne)	Forma zaliczenia
Wykład	15	1	-	-	Egzamin
Laboratorium	15	1	-	-	Zaliczenie na ocenę

Cel przedmiotu

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

Learn how to design and verify event-driven systems.

Wymagania wstępne

Finishing the course of "Discrete process control"

Zakres tematyczny

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).

Metody kształcenia

lecture: classic lecture & discussion

lab: exercises

Efekty uczenia się i metody weryfikacji osiągania efektów uczenia się

Opis efektu	Symbole efektów	Metody weryfikacji	Forma zajęć

Warunki zaliczenia

lecture: passing the exam

lab: positive evaluation of finished exercises

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

Literatura podstawowa

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

Literatura uzupełniająca

Uwagi

Zmodyfikowane przez dr hab. inż. Wojciech Paszke, prof. UZ (ostatnia modyfikacja: 11-04-2022 09:05)