CS453 Automated Software Testing, Fall 14

Announcement

Administrative Information

• Instructor: Moonzoo Kim

Office: 2434 (located at the east wing)

Phone:042-350-3543

E-mail: moonzoo @ c s . k a i s t . a c . k r

Office hour: Tues 10:30 AM-1:30 PM

(reservation e-mail would be preferred)

• Teaching assistants: Shin Hong (hongshin@gmail.com) and Taehoon Kwak (thkwak@kaist.ac.kr)
  

• Lecture hours: Tues & Thurs 9:00 - 10:15 AM
• Lecture room: 114 (N-1)
• Prerequisite: experience in C/C++/Java programming and linux/unix command-line utilities.
• Grading: attendance/class participation/quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
• Late HW will be accepted with 10% penalty of the max score in 1 day, 30% penalty of the max score in 3 days. HW will not be accepted after then (i.e., HW that passes the hard deadline).
• HW should be submitted both in hardcopy and softcopy (through email to TA). 10% penalty of the max score for missing hardcopy or softcopy unless explicitly written in HW. 
• Hint: many questions of exams are from the homework.
• More than 8 absences of class will get F grade
• To start early morning class on time, late attendance shall be considered as 1/3 absence. 
• The official language in the class is English. All students should submit homeworks in English; 10% penalty otherwise
• Questions and answers can be done through Noah BBS
• http://noah.kaist.ac.kr/course/CS453
• Excerpts from 강의평가
• "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
• "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."

Syllabus

 This class covers automated software verification/testing techniques. The goal of the class is to learn practical applications of advanced verification/testing techniques, not sophisticated theories.  These automated techniques can provide high reliability for complex embedded software compared to traditional testing methods in a more productive way.  This class utilizes various software verification/testing tools and learns their underlying mechanisms to produce verification results for the target software.

Course Material

• Textbook
• "Introduction to Software Testing" by P.Ammann and J.Offutt.  Cambridge press 2008
• Reading list
• The Model Checker Spin by G.Holzmann
• Logic in Computer Science 2nd ed by M. Huth and M.RyanLyan
• A Tool for Checking ANSI-C Programs
• DART: Directed Automated Random Testing
• Dictionary for testing terms (한글, English)
• Related tool list
• Spin home page
• CBMC home page 
• MiniSAT home page
• Yices home page
• Z3 home page
• CREST home page
• clang for LLVM
• gcov

Course Schedule

Sep 2 : Introduction

Sep 4: Necessity for systematic & automated testing techniques

Part I: Program coverage criteria and program analysis tools

Sep 11, 16: Graph coverage 

• Intro to Software Testing web site

Sep 18: Graph coverage for source code 

• Understand C++ 

Sep 23: gcov tutorial, CLang tutorial 1/2: Clang AST

• gcov manual

• clang for LLVM

Sep 25: Clang tutorial 2/2: a progam analysis tool by using Clang

Sep 30, Oct 2: Logic coverage

• example

Oct 7:  Logic coverage from source code 

Oct 14: LLVM IR tutorial 1/2

Oct 16: LLVM IR tutorial 2/2

Oct 21: Mid-term exam

Part II: Model checking

Oct 28:SAT-based bounded software model checking

Oct 30: Software model checking examples

Nov  4: Model Checking flash memory storage platform software - an industrial case study

• "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study," IEEE Transactions on Software Engineering (TSE), vol 37, no 2, pages 146-160, March 2011 
• "Formal Verification of a Flash Memory Device Driver- an Experience Report" by M.Kim, Y.Kim, Y.Choi, and H.Kim

Nov 6:Using SAT solver for Sudoku, SAT solver heuristics

• "Sudoku as a SAT problem" by I.Lynce and J.Ouaknine, Intl. Symp. on Artificial Intelligence and Mathematics 2006
• The SuDoku Puzzle as a Satisfiability Problem

Nov 11:  Model checker SPIN part I

Nov 13: Model checker SPIN part II

Nov 25, 27:Linear Temporal Logic

• Principles of the Spin Model Checker by M.Ben-Ari published by Springer

Part III: Concolic testing (a.k.a., dynamic symbolic execution)

Nov 27: Automated SW analysis for high reliability: a Concolic testing approach

• Industrial Application of Concolic Testing on Embedded Software: Case Studies [ICSE'12 paper]
• Automated Unit Testing of Large Industrial Embedded Software using Concolic Testing  [ASE'13 paper] 

Dec 2: CREST Tutorial

Dec 8: CREST Examples,  Busybox application examples through CREST-BV 

Dec 11: Examples of First Order Theories, SMTlib tutorial,

• First order theories (for concolic testing, UML OCL, JML, pre/post condition verification, etc)

• Definition of "theory"
• CS402 Intro to Logic (Predicate Calculus - Semantics)

Dec 16: Final exam

Homeworks

• You need to submit both a hard copy and a soft copy for each homework.
  
• Report box for a hard copy: the report box of top-left corner (#385), 4th floor, N-1
• Email address for a soft copy: send your soft copy to TAs via email (hongshin@gmail.com).
  
• Please put [CS453] at the beginning of the title (ex. [CS453] Homework #1)
  
• You have to use a linux account on verifier<X>.kaist.ac.kr for HW.  See the class noah bbs for detail
• We will try to give you feedback on your homework in 1 week from the hard deadline.
• If you have a question on your HW score, you should contact TA first.

1. HW#1 (structural and dataflow coverage, 100 points): due Sep 25 (Thurs) 23:59
2. HW#2 (coverage testing, 100 points): due Sep 30 (Tues) 23:59

• grep_1.2_v0.zip