Protocol Validation - Lectures
Overview of the material treated in each lecture
Lecture 1
- abstract data types
- basic process algebra
- bisimulation equivalence
- parallelism and communication
- deadlock and encapsulation
- example: a derivation
(Chapters 2, 3.1-3.4)
Lecture 2
- process declarations
- conditional
- summation
- example: Bag
- hidden action and hiding
- branching bisimulation equivalence
- rooted branching bisimulation equivalence
- fair abstraction
- example: Buffers
(Chapters 3.5-3.8, 3.10, 4)
Lecture 3
- verification of buffers
- renaming
- alternating bit protocol
(Chapters 4.3, 3.9, 5.1)
Lecture 4
- linearisation
- state space generation
- hash tables
- Bloom filter
- bitstate hashing
- distributed verification
- homework assignment
(Chapters 6.1-6.3)
Lecture 5
- minimisation modulo branching bisimilarity
- mu-calculus
(Chapters 6.4, 6.6)
Lecture 6
- alternation-free mu-calculus
- regular mu-calculus
- bounded retransmission protocol
(Chapters 6.6, 5.2)
Lecture 7
- linear process equations
- CL-RSP
- invariants
- cones and focus points
(Chapters 6.1, 7.1-7.3)
Lecture 8
- tree identify protocol
- correctness of synchronous tree identify protocol
(Chapters 5.4, 7.4)
Lecture 9
- confluence
- partial order reduction
(Chapters 6.5, 7.5)
Lecture 10
- distributed state space generation
- abstraction
(Chapters 6.7, 6.8)
Lecture 11 is question hour