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