Martin Kot - Modelling and Verification

Modelling and verification

General facts

Guarantee:	Ing. Martin Kot, Ph.D.
Number of credits:	4
Hours:	2/2/0/0
Completition:	Exam
Official web-page:	https://www.cs.vsb.cz/kot/?show=MAV
Lecturers:
Exercisers:

Division of points

Accreditation:	30pts - two projects, 15pts each Condition for accreditation is to obtain some points for at least 1 project
Exam:	70pts - oral exam

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

Annotation

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.

Time table

7:15

8:00

8:45

9:00

9:45

10:30

10:45

11:30

12:15

12:30

13:15

14:00

14:15

15:00

15:45

16:00

16:45

17:30

17:45

18:30

19:15

pondělí

úterý

EA408

Kot M.

středa

čtvrtek

pátek

sobota

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.

Study literature

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

There is a web page http://rsbook.cs.aau.dk devoted to this book which contains some links and some additional useful materials.