Lectures:
Introduction. The notion of reactiveLectures:
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. 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).
Modal logic HML (Henessy-Milner Logic); description of simple system
properties.
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.
Software tool CAAL (Concurrency Workbench, Aalborg Edition).
Solving a small project: modelling of
the alternating bit protocol in CCS, and verification in CAAL.
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
chosen assignment 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.
Exercising semantics of recursive programs by help of fixpoint
computations. Examples of HML-formulas with recursion.
Practical introduction of software tool CAAL.
Preparation for the first small project (alternating bit protocol).
Finalising the project of modelling and verification
of the alternating bit protocol (in CAAL).
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.
Finalising the project of modelling and verification
of a given 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 reactiveLectures:
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. 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).
Modal logic HML (Henessy-Milner Logic); description of simple system
properties.
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.
Software tool CAAL (Concurrency Workbench, Aalborg Edition).
Solving a small project: modelling of
the alternating bit protocol in CCS, and verification in CAAL.
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
chosen assignment 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.
Exercising semantics of recursive programs by help of fixpoint
computations. Examples of HML-formulas with recursion.
Practical introduction of software tool CAAL.
Preparation for the first small project (alternating bit protocol).
Finalising the project of modelling and verification
of the alternating bit protocol (in CAAL).
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.
Finalising the project of modelling and verification
of a given problem in UPPAAL.
Summary of exercises and small projects; discussion regarding the
exam.
Computer labs:
This is contained in the "normal" exercises.