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