The latest offering of the module was in the Academic Year 2010-11.
Assessment: Final 50%, Midterm 20%, Project 30% (Effort 10%, Innovation: 8%, Report writing: 7%, Presentation: 5%).
|
DATES |
Lecture Summary |
Readings |
Resources |
| Week1 |
Introduction to the
module and discussion on Software testing will take place. Software
testing is the mostly widely used validation method and we will start our
discussions with testing. |
For a recent work on symbolic execution based testing, see | Intro.pdf |
| Week 2 | This lecture will focus on software debugging. Lightweight methods like program slicing and fault localization will be discussed briefly. Symbolic execution based methods for debugging will be discussed towards the later parts of the lecture.
|
Relevant chapters of "Why Programs Fail" by Andreas Zeller. In addition: You may read Dynamic Slicing & Relevant Slicing http://www.comp.nus.edu.sg/~abhik/pdf/toplas07.pdfHierarchical Dynamic Slicing http://www.comp.nus.edu.sg/~abhik/pdf/issta07.pdf Software Fault Localization http://www.comp.nus.edu.sg/~abhik/pdf/cc06.pdf |
Debug-1.pdf |
| Week3 |
We will finish the discussion on fault
localization (remaining from previous lecture on debugging) Continuation of the lecture on symbolic execution based software debugging. |
Yesterday my program worked. Today it does not. Why? Andreas Zeller, [ESEC‐FSE 1999]. http://www.infosun.fim.uni‐passau.de/st/papers/tr‐99‐01/esec99‐talk.pdfDARWIN: An Approach for Debugging Evolving Programs Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani, ESEC‐FSE 2009. http://www.comp.nus.edu.sg/~abhik/pdf/fse09.pdf |
Debug-2.pdf |
| Week 4 |
Discussion on
compulsory term project (1 hour) We will discuss program properties and temporal logics. Both linear and branching time logics will be discussed. We will also try to make time for discussing their fixed point characterizations. (1 hour) |
This is the challenge problem we will tackle as the term project in this
module. Every student group will solve the same problem. http://sqrl.mcmaster.ca/pacemaker.htm
The weblink for the
challenge problem we tackle as the course project appears in the module
outline. The project will involve modeling the problem in SPIN model checker
and performing verification. Every group will have to do this (no
other techniques/ tools can be used) --- so that the outputs from
the different groups can be compared in an objective fashion for fair
assessment. This is only the first step and everyone must complete this step
to get any credit in the project. A better project will also use the SPIN
model a guidance to generate C code. SPIN's language is quite close to C ---
so this should be possible. You will also then be able to argue how/why you
could use the SPIN model as guidance and the links between requirements,
model and code. Finally, an excellent project will also have one group
member writing the code without going through modeling and the two codes
will be compared to clarify coding errors or errors in understanding the
requirements. |
|
| Week 5 |
Finish discussion on program properties
and temporal logics. Both linear and branching time logics will be
discussed. We also discussed their recursive characterizations.
|
"Model Checking" by Clarke, Grumberg and Peled, Chapter 3 provides introduction to linear and branching time logics. "Logic in Computer Science" by Huth and Ryan, Chapter 3.9 provides treatment of fixed point characaterizations of CTL properties. |
Temporal Logics |
| Week 6 |
SPIN as a
modeling and validation tool will be discussed in this lecture. This will
also expose the students to the model checking procedure inside SPIN. The
model checker in SPIN checks linear time temporal logics (LTL). A generic
verification method for LTL will be discussed
|
Readings: The Model Checker SPIN, Gerard Holzmann, IEEE Transactions on Software Engineering 97, see http://spinroot.com/gerard/pdf/ieee97.pdf Basic SPIN manual at http://spinroot.com/spin/Man/Manual.html Addtional Readings: You may also want to browse through the book "Design and Validation of Computer Protocols" by Gerard Holzmann. Some details about the verification algorithm of SPIN are available at http://spinroot.com/gerard/pdf/marktoberdorf.pdf The second section of these lecture notes is particularly relevant to the course material.
|
SPIN.pdf |
| Mid Semester Break | |||
| Week 7 | Midterm
Examination (first hour), followed
by discussion on modeling/validation issues in the term project on pacemaker
controller.
|
-- | -- |
| Week 8 | Lesson 8:
CTL model checking algorithm Initiate discussion on software abstractions (in particular predicate abstraction) to be completed in the next lecture.
|
"Model Checking" by Clarke, Grumberg and Peled, Chapter 4. |
CTL-MC.pdf |
| Week 9 | Lesson 9:
Predicate Abstraction -- Generating Finite state Models This lesson will
focus on generating a transition system like model from a program written in
a realistic programming language like C. The transition system like model is
amenable for verification.
|
Reading: Automatic Predicate
Abstraction of C Programs, Thomas Ball, Rupak Majumder, Todd Millstein and
Sriram Rajamani, PLDI 2001, see
http://www.cs.ucla.edu/~rupak/Papers/automatic_abstraction_of_c_programs.ps Additional Reading: If you get time, you can also take a look at the article "Polymorphic Predicate Abstraction" by the same authors at http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSR-TR-2001-10
|
ModelGen.pdf |
| Week 10 | Lesson 11: Abstraction
Refinement: We discuss how to iteratively arrive at the "right" software
abstraction.
|
|
AbstRefine.pdf |
| Week 11 | Lesson 11: PVS theorem
prover: This class will give the students a feel about the issues in
using a proof assistant for program verification.
|
Reading: See the documentation
at
http://pvs.csl.sri.com/documentation.shtml To use the prover, see the
Prover Guide at the PVS web-site (appears under Instructional
Resources). Sections 4 and 5 of the guide (on proof rules and strategies)
are particularly relevant. The System Guide contains some instructions about
getting started. Additional Reading: (optional) Here is an interesting comparison of two well-known theorem provers PVS and HOL by Mike Gordon. See http://www.cl.cam.ac.uk/users/mjcg/PVS.html
|
|
| Week 12 |
Lesson 12: Review of lecture material. Many sample
questions will be discussed as an online session in this lecture.
|
All material covered in the module. |
Past final - 1 |
| Week 13 |
Lesson 13: Project
Presentations by Students.
|
-- | -- |