GS03 Validation and Verification
(MEng code COMP4023)

---

Validation and Verification

Prof. Jonathan P. Bowen

Department of Computer Science
University College London

---

This website is for the Validation and Verification (GS03) module on the Systems Software Engineering MSc (coordinated by David Rosenblum), also 4023 for final year undergraduates, from 8 January to 9 February 2007 (Mondays 2-3pm and 4-5pm, and Fridays 3-5pm - 20 hours total). Graham Roberts will be teaching Mondays 9-10am and Fridays 9-10am in parallel on the module (10 hours total). He will be concentrating on the testing (dynamic analysis) aspects and I will be concentrating on the formal methods (static analysis) aspects. See online GS03 resources. Franco Raimondi will be assisting with the course, especially during Week 3 (see below). Hao Liu will also be assisting with the module during workshops and with problems installing the associated tools.

The recommended textbook is:

Logics in Computer Science: Modelling and Reasoning about Systems. Michael Huth and Mark Ryan. Cambridge University Press. 2nd edition, 2004. ISBN 0 521 54310 X.

This book is essential for the course for reading and exercises (see below).

The following book may also be of interest (especially with respect to Alloy - see below):

Software Abstractions: Logic, Language and Analysis. Daniel Jackson. The MIT Press, 2006. ISBN 0-262-10114-9.

However, this book is not essential and is only relevant to part of the course. There are some copies in the library.

The module will use the following tools:

• Alloy Analyzer (Z-like modelling tool)
  - See FM06 Alloy Tutorial by Daniel Jackson.
• NuSMV (model checker)
  - See local Windows and Linux versions specifically for this module.
• ESC/Java2 (static analysis checker based around the Java Modeling Language (JML), an extension of the Java programming language)

See also:

• Pandora tool (natural deduction proofs)
  - See Friendly e-tutor for Natural Deduction paper.

Note: Links to course material will be added here as the module progresses.

Weekly timetable

Note: The chapters in the Huth and Ryan book have an associated web tutor online. See links for individual chapters below. Please note that this requires a non-Internet Explorer browser to work properly. Download and use Mozilla Firefox or the Netscape browser if you do not already have a suitable alternative web browser. (It has been tested and works with Firefox 1.0.7 and Netscape 7.2 under Windows XP if you have problems.) It is recommended that you work through these exercises after the relevant lecture. Answers to the suggested exercises at the end of the slides are not online, but have been distributed by email.

1. Introduction, propositional and predicate logic (chapters 1 and 2 of Huth & Ryan).
   Slides and exercises:
   - Introduction (notes)
   - Propositional logic (notes)
      - Chapter 1 questions
   - Predicate logic (notes)
      - Chapter 2 questions
   
   
2. Logic for specification and Alloy Analyzer workshop (section 2.7 of Huth & Ryan)
   Slides, examples and coursework:
   - Specifications (notes)
   - Alloy workshop (notes)
   - Alloy examples:
      - Alloy 4 script for Linux (text version)
      - State machine example (text version)
      - Address book example (text version)
   - Coursework 1 on Alloy (deadline Friday, 23 February 2007, worth 5% of the overall marks)
   
   
3. Temporal logic and NuSMV model checking workshop (chapter 3 of Huth & Ryan).
   - Computational Tree Logic and model checking (notes)
      - Chapter 3 questions
   - Coursework 2 on NuSMV (deadline Monday, 26 February 2007, worth 5% of the overall marks)
   Note: This week taught by Franco Raimondi - see teaching information.
   
   
4. Logic for specification and verification of programs (chapter 4 of Huth & Ryan).
   - Specifying and verifying programs (notes)
   - Verifying programs (notes)
      - Chapter 4 questions
   
   
5. Static analysis, ESC/Java workshop and conclusion.
   - Static analysis (notes)
   - ESC/Java2 workshop (notes)

A third piece of coursework on testing (Coursework 3) will be set by Graham Roberts (deadline Monday, 26 February 2007, also worth 5% of the overall marks).

See 2006 exam paper. Although this is dated 2005, it is actually the 2006 exam, and it is the only previous examination paper available. Note that the 2007 examination will be similar in style, but will have less on model checking and more on program verification, in line with the course content about. Further information and guidance was given in the revision classes (see below).

Franco Raimondi gave a revision class on the model checking aspects of the module on Friday 23 February, 2pm, in the Pearson Lecture Theatre, immediately followed at 3pm by a revision class by Graham Roberts on testing aspects in the same location. Jonathan Bowen gave a revision class on all other aspects of the module on Thursday 1 March, 11am, in SB4, 188 Tottenham Court Road. Reports and grades for MSc students (GS03) were issued at this class. These will be distributed to undergraduate students (4023) via email shortly.

Best wishes and good luck for the examination at 10am on Thursday 15 March.

---

Contact information

See also my official UCL web page for contact information.

Background and research

Jonathan Bowen Museophile Limited and a visiting academic in the Department of Computer Science at University College London during 2006-2007. For more information, see www.jpbowen.com. In particular, see my Formal Methods Virtual Library pages. See also a list of publications.

---