1. SylabUZ
2. Faculty of Computer Science, Electrical Engineering and Automatics
3. summer term 2016/2017
4. Automatic Control and Robotics / Computer Control Systems - Second-cycle studies leading to MSc degree
5. Event-driven Systems

Generate PDF for this page

Event-driven Systems - course description

Aim of the course

• zapoznanie studentów ze sposobami formalnej specyfikacji systemów zdarzeniowych;
• ukształtowanie podstaw teoretycznych, niezbędnych do zrozumienia sposobów projektowania, funkcjonowania oraz weryfikacji systemów zdarzeniowych

Prerequisites

Save changes

Sterowanie procesami dyskretnymi

Scope

Nieformalne wprowadzenie do systemów zdarzeniowych.

Podstawy matematyczne. Elementy teorii automatów, niezbędne do formalnej specyfikacji systemów zdarzeniowych. Automat skończony jako model systemu zdarzeniowego. Automaty deterministyczne i niedeterministyczne.

Wprowadzenie do logiki temporalnej. Struktura czasu – czas liniowy i rozgałęzony. Operatory i formuły logiki temporalnej. Logika LTL, CTL, CTL*. Intuicyjne przykłady specyfikacji prostych systemów zdarzeniowych w języku logiki temporalnej.

Zdarzeniowe systemy reaktywne Ogólna koncepcja HCSFM. Realizacja synchroniczna systemów zdarzeniowych. Realizacja asynchroniczna systemów zdarzeniowych.

Formalna weryfikacja specyfikacji systemów zdarzeniowych: Analiza systemu poprzez badanie specyfikacji, zadanej w logikach LTL i CTL. Własności typu „bezpieczeństwo” i „żywotność”. Kontr-przykłady. Metody „model checking”.. Zastosowanie narzędzia typu model checker (na przykładzie NuSMV).

Teaching methods

wykład: wykład konwencjonalny

laboratorium: ćwiczenia laboratoryjne

Learning outcomes and methods of theirs verification

Outcome description	Outcome symbols	Methods of verification	The class form

Assignment conditions

Wykład – warunkiem zaliczenia jest uzyskanie pozytywnej oceny z egzaminu przeprowadzonego w formie pisemnej i ustnej (studia stacjonarne).

Laboratorium – warunkiem zaliczenia jest uzyskanie pozytywnych ocen ze sprawdzianów przygotowania teoretycznego do wykonywania ćwiczeń i sprawozdań z ćwiczeń wskazanych przez prowadzącego zajęcia

Składowe oceny końcowej = wykład: 50% + laboratorium: 50%

Recommended reading

1. R. Klimek, Wprowadzenie do logiki temporalnej, AGH Uczelniane wydawnictwa naukowo-dydaktyczne, Kraków, 1999.
2. I. Grobelna, Weryfikacja modelowa z NuSMV, Oficyna Wydawnicza Uniwersytetu Zielonogórskiego, Zielona Góra, 2011.
3. J. Pecol Embedded Systems. A Contemporary Design Tool, Willey, 2008
4. C. Girault, R. Volk, Petri Nets for Systems Engineering. A Guide to Modeling, Verification and Applications, Springer Verlag, Berlin, 2003

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

Notes

Modified by dr hab. inż. Andrei Karatkevich, prof. UZ (last modification: 16-09-2016 14:00)