Course detail

Model-Based Analysis

FIT-MBAAcad. year: 2023/2024

Introduction of model-base design, testing, analysis and model checking. Petri nets as a model of parallel systems. Techniques for analysis of Petri nets. Markov chains as a model of probabilistic systems. Techniques for analysis of Markov chains. Timed automata as a model of systems working with real-time. Techniques for analysis of timed automata. UML and SysML diagrams within model-based design and techniques for their analysis. Introduction to the tools for analysis of the presented models.

Language of instruction

Czech

Number of ECTS credits

5

Mode of study

Not applicable.

Guarantor

doc. Mgr. Adam Rogalewicz, Ph.D.

Department

Department of Intelligent Systems (UITS)

Entry knowledge

Basic knowledge of graph theory, formal languages concepts and automata theory. Basic knowledge of statistics and probability. Basic knowledge of software engineering.

Rules for evaluation and completion of the course

4 projects (10 points each), final exam (60 points).


Students have to achieve at least 25 points, otherwise the exam is assessed by 0 points.

Aims

Introduce students to the possibility of software (resp. hardware) quality assurance by creating its model, check correctness on the level of the model, and subsequently translate (sometimes automatelly) the model into the target programming language. These principles are introduced on four models, in particular: Petri nets, Markov chains, timed automata and UML/SysML diagrams.

Study aids

Not applicable.

Prerequisites and corequisites

Basic literature

Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008. ISBN: 978-0-262-02649-9
Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640 Dostupné online ze sítě VUT.

Recommended reading

Kaynar, D.,  Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010.  ISBN-13: 978-1608450022 Dostupné online.
Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8-085-86735-4
Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, Springer Verlag, 1993. ISBN: 3-540-60943-1

Elearning

eLearning: currently opened course

Classification of course in study plans

  • Programme IT-MSC-2 Master's

    branch MIS , 2 year of study, summer semester, compulsory-optional
    branch MBS , 0 year of study, summer semester, elective
    branch MPV , 0 year of study, summer semester, elective
    branch MIN , 2 year of study, summer semester, compulsory
    branch MGM , 2 year of study, summer semester, elective
    branch MBI , 0 year of study, summer semester, elective
    branch MSK , 0 year of study, summer semester, elective
    branch MMM , 0 year of study, summer semester, compulsory

  • Programme MITAI Master's

    specialization NISY , 0 year of study, summer semester, elective
    specialization NSPE , 0 year of study, summer semester, elective
    specialization NBIO , 0 year of study, summer semester, elective
    specialization NSEN , 0 year of study, summer semester, compulsory
    specialization NVIZ , 0 year of study, summer semester, elective
    specialization NGRI , 0 year of study, summer semester, elective
    specialization NADE , 0 year of study, summer semester, elective
    specialization NISD , 0 year of study, summer semester, elective
    specialization NMAT , 0 year of study, summer semester, elective
    specialization NSEC , 0 year of study, summer semester, elective
    specialization NISY up to 2020/21 , 0 year of study, summer semester, elective
    specialization NCPS , 0 year of study, summer semester, elective
    specialization NHPC , 0 year of study, summer semester, elective
    specialization NNET , 0 year of study, summer semester, elective
    specialization NMAL , 0 year of study, summer semester, elective
    specialization NVER , 0 year of study, summer semester, compulsory
    specialization NIDE , 0 year of study, summer semester, elective
    specialization NEMB , 0 year of study, summer semester, elective
    specialization NEMB up to 2021/22 , 0 year of study, summer semester, elective

Type of course unit

 

Lecture

26 hod., optionally

Teacher / Lecturer

doc. Mgr. Lukáš Holík, Ph.D.
Ing. Jan Fiedor, Ph.D.
doc. Mgr. Adam Rogalewicz, Ph.D.
doc. RNDr. Milan Češka, Ph.D.

Syllabus

  1. Introduction to the topic of model-based design, testing and analysis. The term model-checking.
  2. P/T Petri nets, definition, evolution rules, state space, bacis problems of analysis, P- and T- invariants.
  3. Analysis of P/T Petri nets, coveribility tree, backward analysis.
  4. Languages and Extensions of P/T Petri nets, Coloured Petri nets. Decidability and relation to Turing machines.
  5. Markov chains as a model of probabilistic systems, Markov chains in discrete and continuous time. Temporal logic for specification of behaviour of Markov chains.
  6. Analysis of Markov chains (model checking).
  7. Extension of Markov chains by nondeterminism - Markov decision processes. Use of Markov chains in theory of operation. Synthesis of operation for Markov decision processes.
  8. Timed automata and their use in modelling of systems with real-time, region abstraction.
  9. Timed temporal logic TCTL and its relation to timed automata.
  10. Decidable problems for Timed automata, simulation and bi-simulation.
  11. UML/SysML diagrams and their use in model-based design and analysis.
  12. Model checking of systems described by UML (state) diagrams.
  13. Mathlab-Simulink, principles of modelling.

Exercise in computer lab

10 hod., compulsory

Teacher / Lecturer

Ing. Jan Fiedor, Ph.D.
doc. Mgr. Lukáš Holík, Ph.D.
Ing. Roman Andriushchenko
doc. Mgr. Adam Rogalewicz, Ph.D.
Ing. Filip Macák

Syllabus

  1. P/T Petri net analysis, Netlab tool (K)
  2. Computation with Marcov chains (N)
  3. Modeling in  PRISM tool (P)
  4. Analysis of timed automata, UPPAAL tool (K)
  5. Modelování v Mathlab-simulink (P)

(P – computer lecture, N – numeric computation, K - combined lecture)

Project

16 hod., compulsory

Teacher / Lecturer

Ing. Roman Andriushchenko
Ing. Jan Fiedor, Ph.D.
doc. Mgr. Adam Rogalewicz, Ph.D.
doc. Mgr. Lukáš Holík, Ph.D.

Syllabus

  1. Application of Petri nets.
  2. Application of Markov chains.
  3. Application of timed automata.
  4. Model in Mathlab-Simulink

Elearning

eLearning: currently opened course