# CS 525, Formal Methods for System Verification

## Autumn, 2006-2007

Instructor

Course Contents (Tentative)

Introduction to Formal Methods

Review of Propositional Logic and Predicate Logic

Verification by Model Checking: LTL, CTL and CTL*

Binary Decision Diagrams and Symbolic Model Checking

Program Verification

Prerequisites

CS203 (Discrete Maths), CS301 (Formal Languages and Automata Theory)

Textbook

M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Second Edition, Cambridge University Press, 2004. (Available in South Asian edition)

Reference Book

Model Checking, Edmund M. Clarke, Orna Grumberg and Doron A. Peled, MIT Press, January 2000.

1.        Course on Bug Catching: Automated Program Verification and Testing at CMU.

2.        Course on Introduction to Model Checking at CMU.

3.        Tutorial on SAT Beyond Propositional Satisfiability by Roberto Sebastiani in CADE 2003.

4.        Linear-Time Temporal Logic and Büchi Automata Tutorial talk by Madhavan Mukund, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997.  (Please read Sections 1 – 3).

5.        Tutorial talk by Madhavan Mukund, Sixth National Seminar on Theoretical Computer Science, Banasthali Vidyapith, Banasthali, Rajasthan, August 1996.

6.        Verification Tools for Finite-State Concurrent Systems, Edmund M. Clarke, Orna Grumberg and David E. Long in REX '93 School/ Workshop: 'A Decade of Concurrency'. Noordwijkerhout, The Netherlands, June 1-4, 1993. Springer Lecture Notes in Computer Science, No. 684, pp. 124-175, 1994.

Class Project

We will use NuSMV to specify and verify a web services atomic transaction protocol. The description of the protocol appears here. You have to do the following tasks:

1.      Download and install NuSMV from the above website, and learn how to use it.

2.      Describe the protocol and its important properties in NuSMV. Specify as many properties as you can.

3.      Verify the model using the NuSMV model checker.

4.      Submit a report (maximum length 5 pages) describing the model and the properties specified and verified. You should discuss important decisions and simplifications made, along with the limitations of SMV (if any) in the modelling exercise.

5.      Submit the SMV model and the results of verification.

Deadline: 3 November, 2006 (Friday). News: The deadline has been extended to 6 November, 2006 (Monday) 6 PM.

No late submissions will be accepted!

The work must be done on your own. Two or more identical or near identical solutions will get zero credit.