CS453 Automated Software Testing, Fall 14
- Final term exam on Dec 16 (Tues) 9:00-11:00 AM at N1 RM# 114
- HW#6 deadline is postponed to Dec 5 (Friday)
- Another make-up class 8:00-10:30 PM Dec 8th (Monday)
- Make-up class 9:00-11:30 PM Nov 25 (Tuesday)
- We will have a global lecture series on model checking and symbolic execution by Prof. Willem Visser (a pioneer of software model checking techniques). I highly recommend you to attend the class.
- Time: Nov 24 (Mon) to 28 (Fri) 2:00 PM - 5:00 PM
- Place: Osangsu seminar room @ the 4th floor of E3-1.
- Instructor: Moonzoo Kim
Office: 2434 (located at the east wing)
Office hour: Tues 10:30 AM-1:30 PM
(reservation e-mail would be preferred)
- Teaching assistants: Shin Hong (firstname.lastname@example.org) and Taehoon Kwak (email@example.com)
- 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
- Excerpts from 강의평가
- "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
- "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."
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.
- "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
Sep 2 : Introduction
Part I: Program coverage criteria and program analysis tools
Sep 11, 16: Graph coverage
Sep 18: Graph coverage for source code
Sep 30, Oct 2: Logic coverage
Oct 14: LLVM IR tutorial 1/2
Oct 16: LLVM IR tutorial 2/2
Oct 21: Mid-term exam
Part II: Model checking
Oct 30: Software model checking examples
- "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
- "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)
- 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
- First order theories (for concolic testing, UML OCL, JML, pre/post condition verification, etc)
Dec 16: Final exam
- 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 (firstname.lastname@example.org).
- 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.
- HW#1 (structural and dataflow coverage, 100 points): due Sep 25 (Thurs) 23:59
- HW#2 (coverage testing, 100 points): due Sep 30 (Tues) 23:59