CS 525, Formal Methods
for System Verification
Autumn, 2006-2007
Instructor Purandar Bhaduri, ext: 2360, email: pbhaduri. 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, Reference Book Model
Checking,
Edmund M. Clarke, Orna Grumberg and Doron A. Peled, MIT Press, January 2000. Some Useful Links 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, 5. Finite-state Automata on Infinite Inputs, 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 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. |