Title:  ModelBased Analysis 

Code:  MBA 

Ac.Year:  2019/2020 

Sem:  Summer 

Curriculums:  

Language of Instruction:  Czech 

Credits:  5 

Completion:  examination (written&oral) 

Type of instruction:  Hour/sem  Lectures  Seminar Exercises  Laboratory Exercises  Computer Exercises  Other 

Hours:  39  0  0  6  7 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  70  0  0  0  30 



Guarantor:  Rogalewicz Adam, doc. Mgr., Ph.D. (DITS) 

Deputy guarantor:  Češka Milan, prof. RNDr., CSc. (DITS) 

Lecturer:  Češka Milan, RNDr., Ph.D. (DITS) Rogalewicz Adam, doc. Mgr., Ph.D. (DITS) 
Faculty:  Faculty of Information Technology BUT 

Department:  Department of Intelligent Systems FIT BUT 

Prerequisites:  

Schedule: 

Day  Lesson  Week  Room  Start  End  Lect.Gr.  Groups 

Tue  lecture  lectures  A113  17:00  19:50  1MIT 2MIT  MIN MMM xx 
  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.
 Description: 

  Introduction of modelbase 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 realtime. Techniques for analysis of timed automata. UML and SysML diagrams within modelbased design and techniques for their analysis. Introduction to the tools for analysis of the presented models.
 Knowledge and skills required for the course: 

  Basic knowledge of graph theory, formal languages concepts and automata theory. Basic knowledge of statistics and probability. Basic knowledge of software engineering.
 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 safetycritical 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.
 Syllabus of lectures: 

 
Introduction to the topic of modelbased design, testing and analysis. The term
modelchecking.

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 realtime.
 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 modelbased 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.
 Fundamental literature: 

  Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0387137238
 Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8085867354
 Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory
of Timed I/O Automata, Morgan & Claypool, 2010. ISBN13:
9781608450022
 Boucherie,
R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in
Practice, Springer, 2017. ISBN13: 9783319477640
 Study literature: 

  Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0387137238
 Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8085867354
 Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, Springer Verlag, 1993. ISBN: 3540609431
 Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory
of Timed I/O Automata, Morgan & Claypool, 2010. ISBN13:
9781608450022 Available online.
 Boucherie,
R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in
Practice, Springer, 2017. ISBN13: 9783319477640 Available online from VUT network.
 Controlled instruction: 

  3 projects, 10 points each.
 
