Course detail
Model-Based Analysis
FIT-MBAAcad. year: 2020/2021
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
Number of ECTS credits
Mode of study
Guarantor
Department
Learning outcomes of the course unit
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Course curriculum
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Students have to achieve at least 30 points, otherwise the exam is assessed by 0 points.
Recommended optional programme components
Prerequisites and corequisites
- recommended prerequisite
Theoretical Computer Science
Basic literature
Recommended 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.
Elearning
Classification of course in study plans
- Programme IT-MSC-2 Master's
branch MGM , 2 year of study, summer semester, elective
branch MBI , 0 year of study, summer semester, elective
branch MBS , 0 year of study, summer semester, elective
branch MIN , 2 year of study, summer semester, compulsory
branch MIS , 2 year of study, summer semester, compulsory-optional
branch MMM , 0 year of study, summer semester, compulsory
branch MPV , 0 year of study, summer semester, elective
branch MSK , 0 year of study, summer semester, elective - Programme MITAI Master's
specialization NISY , 0 year of study, summer semester, elective
specialization NADE , 0 year of study, summer semester, elective
specialization NBIO , 0 year of study, summer semester, elective
specialization NCPS , 0 year of study, summer semester, elective
specialization NEMB , 0 year of study, summer semester, elective
specialization NHPC , 0 year of study, summer semester, elective
specialization NGRI , 0 year of study, summer semester, elective
specialization NIDE , 0 year of study, summer semester, elective
specialization NISD , 0 year of study, summer semester, elective
specialization NMAL , 0 year of study, summer semester, elective
specialization NMAT , 0 year of study, summer semester, elective
specialization NNET , 0 year of study, summer semester, elective
specialization NSEC , 0 year of study, summer semester, elective
specialization NSEN , 0 year of study, summer semester, compulsory
specialization NSPE , 0 year of study, summer semester, elective
specialization NVER , 0 year of study, summer semester, compulsory
specialization NVIZ , 0 year of study, summer semester, elective
Type of course unit
Lecture
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.
- 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.
- Temporal logic PCTL for Markov chain specification. Advanced analysis of Markov chains and Markov Decision Processes.
- Using counter-examples in the verification of Markov Chains. Synthesis of Markov chains.
- Continuous-time Markov chains and their analysis using uniformization.
- 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
Teacher / Lecturer
Syllabus
- Analysis of P/T Petri nets, tools NetLab a PIPE.
- Analysis of Markov chains, tool PRISM
- Analysis of timed automata, tool UPPAAL.
Project
Teacher / Lecturer
Syllabus
- Application of Petri nets.
- Application of timed automata.
- Application of Markov chains.
Elearning