CS5219 Automated Software Validation

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

Testing.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.pdf

 Hierarchical 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.pdf

DARWIN: 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.
 

 

Term Project Notes

 

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.

 


Reading:  Generating Abstract Explanations of Spurious Counterexamples in C Programs by Ball and Rajamani at http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSR-TR-2002-09

 

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

 

PVS.pdf

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

Past final - 2

Week 13 Lesson 13: Project Presentations by Students.

 

-- --