Software Verification and testing.

I'll be lecturing on Mondays at 2:10 in SG-LT08. Tutorials will be on Tuesdays 4:10pm. Lecture slides will be posted after each lecture, sometimes before.

Reading weeks are 3 and 12.

Lecture week 1.
Lecture week 2.
Lecture week 4.
Lecture slides week 5, part 1 and part 2.
Lecture slides week 6, part 1 and part 2.
Lecture slides week 7.
Lecture slides week 8.
Lecture slides week 9, announcement: PhD funding opportunities (slides written by Georg Struth).
Lecture slides week 10, part 1 part 2.
Lecture slides week 11.

Solution to the exercise and (possible) commonly-made errors are available here. Books and papers you can read for this module were mentined in the lectures and are available in the slides.

A commentary to Potter book (written by Martin Cooke) could help you understand the material better.

An additional book you could use to help you with Z is The Z Notation: A Reference Manual (on www), J.M. Spivey, Prentice Hall, 2nd edition, 1992.

A paper about statecharts is called The STATEMATE Semantics of Statecharts" David Harel, A. Naamad, ACM TOSEM, 5(4), 293-333 - 1996. You can find it on Google.

Tutorials

The tutorial sheets are available in the pdf format.

Answers some to tutorial questions in weeks 2..4 are available in the following (these solutions may use elements of the Z notation which are outside the scope of the module - during the tutorials I've shown you solutions using what I introduced)

Potter's book (to some questions)
In the commentary (written by Martin Cooke) mentioned above (the pages of the commentary with answers are also available as pdf), with the following changes,
- Question 4.10, answers for parts 1..4 have to be enclosed in curly brackets,
  1. {(red, red) (red, blue) (blue, red) (blue, blue)}
  2. {( {round}, {round} )}
  3. {(red,{round}) (blue,{round})}
  4. {({round}, red) ({round}, blue)}
- Question 5.3, part ii should be:
```
{}[A]<->{}[A]
== P( {}[A] x {}[A] )
== P( {}[A x A] )
== {{}[A x A] }
```
- Question 5.5, part ii should be:
  dom plays is of type PPeople
  dom worskby is of type PInstrument
  ran plays is of type PInstrument
  ran worksby is of type PActions
  Above, P stands for "powerset".
- Question 5.7, part iv should be:
  domain is { {Alice, Ben, Huw }, {Ben}, {} }
  and the range is { Bicycle, Unicycle, Tricycle }
- Question 5.7, answers to the three parts at the bottom are:

For other weeks, I've shown you solutions during the tutorials.
Exam questions and answers for years 2001-2002 and 2002-2003 are available here. Questions for the two recent years are available on departmental web pages, here.

email me (replace _ in the email address with @)