Course details

# Model-Based Analysis

MBA Acad. year 2021/2022 Summer semester 5 credits

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.

Guarantor

Deputy Guarantor

Language of instruction

Completion

Time span

Assessment points

Department

Lecturer

Češka Milan, prof. RNDr., CSc. (DITS FIT BUT)

Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)

Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)

Course Web Pages

Learning objectives

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.

Why is the course taught

The classical approach to software development is to implement it in a chosen programming language and then test it (eventually verify it). In the quality assurance of embedded and safety-critical systems is often used a different approach. First, one creates a model of the system (or its part) in a suitable modelling language and then verify its quality on the level of the model. After that one translate (often automatically) the model into the target programming language. Verification on the level of a model is often much easier then verification of equal properties directly on the level of a source code.

Prerequisites

Prerequisite kwnowledge and skills

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

Study literature

- Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
- Č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
- Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010. ISBN-13: 978-1608450022 Available online.
- Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640 Available online from VUT network.
- Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008. ISBN: 978-0-262-02649-9

Fundamental literature

- Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
- Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8-085-86735-4
- Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010. ISBN-13: 978-1608450022
- Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640

Syllabus of lectures

- Introduction to the topic of model-based design, testing and analysis. The term model-checking.
- Petri nets. Basic terms, history and applications.
- P/T Petri nets, definition, evolution rules, state space, bacis problems of analysis.
- Analysis of P/T Petri nets, coveribility tree, P- and T- invariants.
- Extensions of P/T Petri nets and Coloured Petri nets. Decidability and relation to Turing machines. Tools NetLab a PIPE.
- Markov chains as a model of probabilistic systems, Markov chains in discrete and continuous time. Temporal logic for specification of behaviour of Markov chains.
- Analysis of Markov chains (model checking), the tool PRISM.
- Extension of Markov chains by nondeterminism - Markov decision processes. Use of Markov chains in theory of operation. Synthesis of operation for Markov decision processes.
- Timed automata and their use in modelling of systems with real-time.
- Timed automata analysis, region abstraction, decidable problems. Tool UPPAAL.
- Timed temporal logic TCTL and its relation to timed automata.
- UML/SysML diagrams and their use in model-based design and analysis.
- Model checking of systems described by UML (state) diagrams.

Syllabus of computer exercises

If applicable:

- Analysis of P/T Petri nets, tools NetLab a PIPE.
- Analysis of Markov chains, tool PRISM
- Analysis of timed automata, tool UPPAAL.

Syllabus - others, projects and individual work of students

- Application of Petri nets.
- Application of Markov chains.
- Application of timed automata.

Controlled instruction

3 projects, 10 points each.

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

Schedule

Course inclusion in study plans

- Programme IT-MSC-2, field MBI, MBS, MPV, MSK, any year of study, Elective
- Programme IT-MSC-2, field MGM, 2nd year of study, Elective
- Programme IT-MSC-2, field MIN, 2nd year of study, Compulsory
- Programme IT-MSC-2, field MIS, 2nd year of study, Compulsory-Elective group F
- Programme IT-MSC-2, field MMM, any year of study, Compulsory
- Programme MITAI, specialisation NADE, NBIO, NCPS, NEMB, NGRI, NHPC, NIDE, NISD, NISY, NMAL, NMAT, NNET, NSEC, NSPE, NVIZ, any year of study, Elective
- Programme MITAI, specialisation NSEN, NVER, any year of study, Compulsory