Gurantor department | Department of Computer Science | Credits | 4 |

Subject guarantor | prof. RNDr. Petr Jančar, CSc. | Subject version guarantor | prof. RNDr. Petr Jančar, CSc. |

Study level | undergraduate or graduate | Requirement | Optional |

Year | 1 | Semester | winter |

Study language | Czech | ||

Year of introduction | 2007/2008 | Year of cancellation | 2009/2010 |

Intended for the faculties | FEI | Intended for study types | Follow-up Master |

Instruction secured by | |||
---|---|---|---|

Login | Name | Tuitor | Teacher giving lectures |

JAN59 | prof. RNDr. Petr Jančar, CSc. | ||

KOT06 | Ing. Martin Kot, Ph.D. |

Extent of instruction for forms of study | ||
---|---|---|

Form of study | Way of compl. | Extent |

Full-time | Credit and Examination | 2+2 |

Part-time | Credit and Examination | 10+4 |

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).

Lectures

Tutorials

Project work

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.

Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, August 2007.

Solving and discussing the written tasks for each tutorial.
Elaborating two miniprojects with assistence, finished by individual written reports.
Final exam (oral, with a written preparation).

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

Subject has no prerequisities.

Subject has no co-requisities.

Lectures:
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.
Complete definition of the language CCS (syntax and sematics),
examples. CCS with variables.
Behavioural equivalences (i.e., the notion of equivalent behaviour
of systems). Trace equivalence. Bisimulation equivalence; bisimulation
games.
Properties of strong bisimilarity. Internal actions. Weak
bisimilarity. An example (a small communication protocol).
Software tool Concurrency Workbench, CWB (Edinburgh, UK).
Modal logic HML (Henessy-Milner Logic); description of simple system
properties.
Further examples in CWB.
Correspondence of bisimulation equivalence and HM-logic.
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.
Solving a small project: modelling of
the alternating bit protocol in CCS, and verification in CWB.
Timed labelled transition systems.
Timed CCS. Timed automata.
Timed and untimed bisimulation equivalence.
Construction of regions at timed automata.
HM-logic with time.
Software tool UPPAAL (based on timed automata).
Modelling, specification, simulation and verification in UPPAAL on
practical examples.
Solving a small project: modelling and analysis of
`gossiping girls' in UPPAAL.
Information about other types of verifikation.
Summary of the course. Information about the exam.
Exercises:
Construction of simple labelled transition systems and description
in CCS.
Examples of small systems described in CCS.
Informal discussion of (non)equivalence of their behaviours.
Exercising the notion of bisimilarity by bisimulation games on
small transition systems.
Proofs of weak bisimilarity of small systems (with pencil and
paper).
Expressing simple system properties in HM-logic.
Practical introduction of software tool CWB.
Exercising semantics of recursive programs by help of fixpoint
computations.
Examples of HML-formulas with recursion.
Preparation for the first small project (alternating bit protocol).
Finalising the project of modelling and verification
of the alternating bit protocol (in CWB).
Examples of small timed systems,
described in timed CCS and by help of timed automata.
Examples of equivalent systems with respect to timed bisimulation
equivalence. Computation of regions at timed automata.
Practical introduction of software tool UPPAAL.
Preparation for the second small project (`gossiping girls').
Finalising the project of modelling and verification
of the `gossiping girls' problem (in UPPAAL).
Summary of exercises and small projects; discussion regarding the
exam.
Computer labs:
This is contained in the "normal" exercises.

Task name | Type of task | Max. number of points
(act. for subtasks) | Min. number of points |
---|---|---|---|

Exercises evaluation and Examination | Credit and Examination | 100 (100) | 51 |

Exercises evaluation | Credit | 30 (30) | 10 |

První projekt (CWB) | Project | 15 | 10 |

Druhý projekt (UPPAAL) | Project | 15 | 10 |

Examination | Examination | 70 | 25 |

Show history

Academic year | Programme | Field of study | Spec. | Zaměření | Form | Study language | Tut. centre | Year | W | S | Type of duty | |
---|---|---|---|---|---|---|---|---|---|---|---|---|

2009/2010 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Optional | study plan | ||||

2009/2010 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Optional | study plan | ||||

2008/2009 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Optional | study plan | ||||

2008/2009 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Optional | study plan | ||||

2007/2008 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | P | Czech | Ostrava | 1 | Optional | study plan | ||||

2007/2008 | (N2647) Information and Communication Technology | (2612T025) Computer Science and Technology | K | Czech | Ostrava | 1 | Optional | study plan |

Block name | Academic year | Form of study | Study language | Year | W | S | Type of block | Block owner |
---|