SylabUZ

Wygeneruj PDF dla tej strony

Systemy zdarzeniowe - opis przedmiotu

Informacje ogólne
Nazwa przedmiotu Systemy zdarzeniowe
Kod przedmiotu 11.9-WE-AiRD-SD
Wydział Wydział Informatyki, Elektrotechniki i Automatyki
Kierunek Automatyka i robotyka / Komputerowe Systemy Automatyki
Profil ogólnoakademicki
Rodzaj studiów drugiego stopnia z tyt. magistra inżyniera
Semestr rozpoczęcia semestr zimowy 2020/2021
Informacje o przedmiocie
Semestr 1
Liczba punktów ECTS do zdobycia 3
Typ przedmiotu obowiązkowy
Język nauczania polski
Sylabus opracował
  • dr inż. Iwona Grobelna
  • dr inż. Grzegorz Łabiak
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 9 0,6 Egzamin
Laboratorium 15 1 9 0,6 Zaliczenie na ocenę

Cel przedmiotu

  • 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

Wymagania wstępne

Zaliczenie przedmiotu "Sterowanie procesami dyskretnymi"

Zakres tematyczny

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

Metody kształcenia

wykład: wykład konwencjonalny

laboratorium: ćwiczenia laboratoryjne

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

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

Warunki zaliczenia

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%

Literatura podstawowa

  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

Literatura uzupełniająca

  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)

Uwagi


Zmodyfikowane przez dr hab. inż. Wojciech Paszke, prof. UZ (ostatnia modyfikacja: 29-04-2020 18:24)