1 of 6

​

Software (in-)Correctness Analysis

Lecture-6

​

Ganesh Gopalakrishnan

2 of 6

Safety and Liveness

  • Rozier, Page 179 on Safety
  • Rozier, Page 180 on Liveness
  • Rozier, Page 182, Examples

3 of 6

Really useful tricks with model-checkers

  • We will show that writing test-benches for simulation is HARD
    • Requires expertise
    • You miss many cases
  • Properties are ideal test-benches in some sense
    • You are focused on a few variables
      • You state something deep
        • The model-checker _has_ to discover how to show the that the property is true
        • OR it has to show you a failure
      • This way you slowly walk up the protocol
  • When finally you have an invariant, you can generate and get copious tests!
    • Let's try this also

4 of 6

The man,wolf,cabbage,goat problem in Murphi

learn to model + check in Murphi and also in SPIN

Murphi available as "rumur" - Utah's random-walk version is ROMP

5 of 6

mwgc

6 of 6

Let us study Promela in Practice

  • We will develop a model for a distributed locking protocol
  • It will exhibit many features of Promela
  • We will find a property not verifying correctly
    • You'll be invited to find a fix
    • Assignment-3 issues during Lecture-7
    • There coud be another protocol also in Asg-3
      • Maybe Distributed Termination of Dijkstra
    • In Asg-3
      • I plan to have you verify some of Thomas Wahl's conjectures
  • With Asg3, we will say bye to Promela/SPIN and then visit Murphi, and then the other mode-checkers
  • For the remainder of the lecture, plz see locking-prot.pdf and locking-buggy.pml in this directory in the directory Lec6Handouts in here

​