## CS 525, Formal Methods
for System Verification
## Autumn, 2006-2007
Purandar Bhaduri, ext: 2360, email: pbhaduri.
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
CS203 (Discrete Maths), CS301 (Formal Languages and Automata Theory)
M. Huth and M. Ryan,
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 4.
Linear-Time
Temporal Logic and Büchi Automata 5.
Finite-state
Automata on Infinite Inputs 6.
Verification
Tools for Finite-State Concurrent Systems, Edmund M. Clarke, Orna
Grumberg and David E. Long in REX Springer Lecture Notes in Computer Science, No.
684, pp. 124-175, 1994.
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). 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. |