1 of 3

​

Software (in-)Correctness Analysis

Lecture-4

​

Ganesh Gopalakrishnan

2 of 3

We want to verify properties specified formally

  • We will introduce temporal logic
  • Then we will go through a Leader Election role-play
    • Walk thru the example in
      • Spin/Examples/leader0.pml
        • This came with the SPIN distribution
      • Also look at README_tests.txt in the same folder
        • This has a nice tutorial walk thru many examples
      • We will create leader1.pml from leader0.pml as follows
        • Generate a never automaton via
          • spin -f "!(noL U [] oneL)"
            • If in doubt, see what spin -f does on "[]x" and "<>x"
              • to see if it inverts the logic for you
  • Class lecture
    • Leader role-play
    • Walk-thru Figure 23.10
      • How does it become the situation of 23.11
        • Section 23.4.1
      • Nested DFS of Figure 23.12

3 of 3

We want to verify properties specified formally

  • Encode 23.11 in Promela
    • Check using never automata
      • Look at error trail
  • Now look at Leader Election code
    • Walk thru it
      • Run it
        • Break it and run it
  • Now go thru PhilLL.pml
    • It has command-line runs
      • Go thru it
  • Now go thru README_tests.txt

​

Asg-2 will be on

Figure 23.9 , Problem 22.5 , Figure 415, questions on nested DFS