460-4016/01 – Modeling and Verification (MaV)

Gurantor departmentDepartment of Computer ScienceCredits4
Subject guarantorIng. Martin Kot, Ph.D.Subject version guarantorIng. Martin Kot, Ph.D.
Study levelundergraduate or graduateRequirementOptional
Year2Semesterwinter
Study languageCzech
Year of introduction2010/2011Year of cancellation
Intended for the facultiesFEIIntended for study typesFollow-up Master
Instruction secured by
LoginNameTuitorTeacher giving lectures
KOT06 Ing. Martin Kot, Ph.D.
Extent of instruction for forms of study
Form of studyWay of compl.Extent
Full-time Credit and Examination 2+2
Part-time Credit and Examination 14+4

Subject aims expressed by acquired skills and competences

On successful completion of the course, the student - knows the basic notions in the area of modelling with the calculus of communicating systems (CCS) and timed automata, - understands the basic theory needed for modelling and verification of systems, including the bisimulation equivalence, - is able to express commonly tested properties of systems by temporal logic formulas, - manages to work with selected modelling and verification software tools, - is able to analyze, model and verify small practical systems (like communication protocols).

Teaching methods

Lectures
Tutorials

Summary

Problem of correctness, i.e. the problem of verification that a given computer (hardware and/or software) system has the properties required by its specification, belongs to the fundamental problems of practical and theoretical computer science. The continuing development of information technologies leads to constructing systems with increasing complexity, and thus both research and industrial practice need solidly based verification procedures. Automated verification, comprising also so called `model checking', was established as a class of methods successfully applied in practice during the 1990s. In model checking, the property to be tested is expressed, e.g., in a simple temporal logic, and is verified by (semi)automatic methods on a system model. The aim of the course is to explain the basic principles of this (automated) verification, and to demonstrate them on models of concrete practical problems, for which suitable freely available software verification products exist.

Compulsory literature:

1. Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, August 2007. 2. Gerd Behrmann, Alexandre David, Kim G. Larsen: A Tutorial on Uppaal 4.0. Available online at https://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf [14.4.2021]

Recommended literature:

1. Gerard J. Holzmann: The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley, 2003 2. Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.

Way of continuous check of knowledge in the course of semester

Solving and discussing the written tasks for each tutorial. Elaborating two miniprojects with assistence, finished by creating files used as input for verification tools. Final exam (oral, with a written preparation).

E-learning

Electronic materials underlying the lectures and tutorials, pointers to software tools, and futher information are accessible from the course web-page.

Other requirements

No additional requirements are placed on the student.

Prerequisities

Subject has no prerequisities.

Co-requisities

Subject has no co-requisities.

Subject syllabus:

Lectures: 1. Introduction. The notion of reactive systems, examples. Labelled transition systems as a basic model. Informal introduction into the language CCS (Calculus of Communicating Systems) for description of reactive systems. 2. Complete definition of the language CCS (syntax and sematics), examples. CCS with variables. 3. Behavioural equivalences (i.e., the notion of equivalent behaviour of systems). Trace equivalence. Bisimulation equivalence; bisimulation games. 4. Properties of strong bisimilarity. Internal actions. Weak bisimilarity. An example (a small communication protocol). 5. Modal logic HML (Henessy-Milner Logic); description of simple system properties. 6. The use of the abstract notion of fixpoints in complete lattices for defining semantics of recursive programs. Computation of bisimulation equivalence as a fixpoint. HM-logic with recursion; a game characterization. Correspondence of bisimulation equivalence and HM-logic. 7. Software tool CAAL (Concurrency Workbench, Aalborg Edition). 8. Solving a small project: modelling of the alternating bit protocol in CCS, and verification in CAAL. 9. Timed labelled transition systems. Timed CCS. Timed automata. 10. Timed and untimed bisimulation equivalence. Construction of regions at timed automata. HM-logic with time. 11. Software tool UPPAAL (based on timed automata). Modelling, specification, simulation and verification in UPPAAL on practical examples. 12. Solving a small project: modelling and analysis of chosen assignment in UPPAAL. 13. Information about other types of verifikation. Summary of the course. Information about the exam. Exercises: 1. Construction of simple labelled transition systems and description in CCS. 2. Examples of small systems described in CCS. Informal discussion of (non)equivalence of their behaviours. 3. Exercising the notion of bisimilarity by bisimulation games on small transition systems. 4. Proofs of weak bisimilarity of small systems (with pencil and paper). 5. Expressing simple system properties in HM-logic. 6. Exercising semantics of recursive programs by help of fixpoint computations. Examples of HML-formulas with recursion. 7. Practical introduction of software tool CAAL. Preparation for the first small project (alternating bit protocol). 8. Finalising the project of modelling and verification of the alternating bit protocol (in CAAL). 9. Examples of small timed systems, described in timed CCS and by help of timed automata. 10. Examples of equivalent systems with respect to timed bisimulation equivalence. Computation of regions at timed automata. 11. Practical introduction of software tool UPPAAL. Preparation for the second small project. 12. Finalising the project of modelling and verification of a given problem in UPPAAL. 13. Summary of exercises and small projects; discussion regarding the exam. Computer labs: This is contained in the "normal" exercises.

Conditions for subject completion

Full-time form (validity from: 2010/2011 Winter semester, validity until: 2015/2016 Summer semester)
Task nameType of taskMax. number of points
(act. for subtasks)
Min. number of pointsMax. počet pokusů
Exercises evaluation and Examination Credit and Examination 100 (100) 51
        Exercises evaluation Credit 30 (30) 10
                First project (CWB) Project 15  10
                Second project (UPPAAL) Project 15  10
        Examination Examination 70  25 3
Mandatory attendence participation:

Show history

Conditions for subject completion and attendance at the exercises within ISP:

Show history

Occurrence in study plans

Academic yearProgrammeBranch/spec.Spec.ZaměřeníFormStudy language Tut. centreYearWSType of duty
2024/2025 (N0613A140034) Computer Science TI P Czech Ostrava 1 Choice-compulsory type B study plan
2024/2025 (N0613A140034) Computer Science TI K Czech Ostrava 1 Choice-compulsory type B study plan
2023/2024 (N0613A140034) Computer Science TI K Czech Ostrava 1 Choice-compulsory type B study plan
2023/2024 (N0613A140034) Computer Science TI P Czech Ostrava 1 Choice-compulsory type B study plan
2023/2024 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2023/2024 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2022/2023 (N0613A140034) Computer Science TI K Czech Ostrava 1 Choice-compulsory type B study plan
2022/2023 (N0613A140034) Computer Science TI P Czech Ostrava 1 Choice-compulsory type B study plan
2022/2023 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2022/2023 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2021/2022 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2021/2022 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2020/2021 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2020/2021 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2019/2020 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2019/2020 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2018/2019 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2018/2019 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2017/2018 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2017/2018 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2016/2017 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2016/2017 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2015/2016 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Choice-compulsory study plan
2015/2016 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Choice-compulsory study plan
2014/2015 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 2 Optional study plan
2014/2015 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Optional study plan
2013/2014 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 2 Optional study plan
2013/2014 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Optional study plan
2012/2013 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 2 Optional study plan
2012/2013 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Optional study plan
2011/2012 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Optional study plan
2011/2012 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Optional study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology P Czech Ostrava 1 Optional study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology K Czech Ostrava 1 Optional study plan
2010/2011 (N2647) Information and Communication Technology (2612T025) Computer Science and Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (2601R004) Measurement and Control Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (2602R014) Applied and Commercial Electronics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (3901R039) Biomedical Technician (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2649) Electrical Engineering (3907R001) Electrical Power Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (1103R031) Computational Mathematics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2601R013) Telecommunication Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2612R025) Computer Science and Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (B2647) Information and Communication Technology (2612R059) Mobile Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (1103T031) Computational Mathematics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (2601T013) Telecommunication Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2647) Information and Communication Technology (2612T059) Mobile Technology (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (2601T004) Measurement and Control Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (2612T015) Electronics (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (3901T009) Biomedical Engineering (01) Exchange Students P Czech Ostrava Optional study plan
2010/2011 (N2649) Electrical Engineering (3907T001) Electrical Power Engineering (01) Exchange Students P Czech Ostrava Optional study plan

Occurrence in special blocks

Block nameAcademic yearForm of studyStudy language YearWSType of blockBlock owner

Assessment of instruction



2020/2021 Summer
2014/2015 Winter
2011/2012 Winter