Course detail
Model-Based Analysis
FIT-MBAAcad. year: 2019/2020
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.
Supervisor
Department
Learning outcomes of the course unit
Not applicable.
Prerequisites
Basic knowledge of graph theory, formal languages concepts and automata theory. Basic knowledge of statistics and probability. Basic knowledge of software engineering.
- recommended prerequisite
Co-requisites
Not applicable.
Recommended optional programme components
Not applicable.
Recommended or required reading
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 Dostupné online.
Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640 Dostupné online (https://link.springer.com/book/10.1007%2F978-3-319-47766-4) ze sítě VUT.
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
Č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
Planned learning activities and teaching methods
Not applicable.
Assesment methods and criteria linked to learning outcomes
Not applicable.
Language of instruction
Czech
Work placements
Not applicable.
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.
Specification of controlled education, way of implementation and compensation for absences
3 projects, 10 points each.
Students
have to achieve at least 30 points, otherwise the exam is assessed by 0 points.
Classification of course in study plans
- Programme IT-MGR-2 Master's
branch MBI , any year of study, summer semester, 5 credits, optional
branch MPV , any year of study, summer semester, 5 credits, optional
branch MSK , any year of study, summer semester, 5 credits, optional
branch MBS , any year of study, summer semester, 5 credits, optional
branch MMM , any year of study, summer semester, 5 credits, compulsory - Programme MITAI Master's
specialization NADE , any year of study, summer semester, 5 credits, optional
specialization NBIO , any year of study, summer semester, 5 credits, optional
specialization NGRI , any year of study, summer semester, 5 credits, optional
specialization NNET , any year of study, summer semester, 5 credits, optional
specialization NVIZ , any year of study, summer semester, 5 credits, optional
specialization NCPS , any year of study, summer semester, 5 credits, optional
specialization NSEC , any year of study, summer semester, 5 credits, optional
specialization NEMB , any year of study, summer semester, 5 credits, optional
specialization NHPC , any year of study, summer semester, 5 credits, optional
specialization NISD , any year of study, summer semester, 5 credits, optional
specialization NIDE , any year of study, summer semester, 5 credits, optional
specialization NISY , any year of study, summer semester, 5 credits, optional
specialization NMAL , any year of study, summer semester, 5 credits, optional
specialization NMAT , any year of study, summer semester, 5 credits, optional
specialization NSEN , any year of study, summer semester, 5 credits, compulsory
specialization NVER , any year of study, summer semester, 5 credits, compulsory
specialization NSPE , any year of study, summer semester, 5 credits, optional - Programme IT-MGR-2 Master's
branch MGM , 2. year of study, summer semester, 5 credits, optional
branch MIS , 2. year of study, summer semester, 5 credits, compulsory-optional
branch MIN , 2. year of study, summer semester, 5 credits, compulsory
Type of course unit
Lecture
39 hours, optionally
Teacher / Lecturer
Syllabus
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.
Exercise in computer lab
6 hours, compulsory
Teacher / Lecturer
Syllabus
If applicable:
- Analysis of P/T Petri nets, tools NetLab a PIPE.
- Analysis of Markov chains, tool PRISM
- Analysis of timed automata, tool UPPAAL.
Project
7 hours, compulsory
Teacher / Lecturer
Syllabus
- Application of Petri nets.
- Application of Markov chains.
- Application of timed automata.
eLearning
eLearning: currently opened course