CS453 Automated Software Testing, Fall 13
Announcement
- Sep 14: No class on Sep 17. Happy Chuseok!
- Sep 26: A report box for homwork is created at box #392, 4th floor, N1 building
- Oct 1: HW2 is released. I prepared linux machines for your programming homework. Please see Noah BBS.
- Oct 15: Midterm exam on Oct 31 (Thurs) 9:00 - 10:15 AM
- Oct 15: No class on Nov 5th (Tues) due to visiting HKUST for CS dept. seminar.
- Oct 15: We will have make-up classes on Oct 24 at regular class time.
- Dec 16: Final exam on Dec 17 (Tue) 9:00 AM - 12:00 PM
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: 박용배 (Yongbae Park) yongbae2 @ g m a i l . c o m
- Lecture hours: Tues & Thurs 9:00 - 10:15 AM
- Lecture room: 113 (N-1)
- Prerequisite: experience in C/C++ programming and linux/unix command-line utilities.
- Grading: attendance/class participation/quiz: 20%, HW: 50%, midterm exam: 15%, final exam:15%
- Late HW is 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.
- HW should be submitted both in hardcopy and softcopy (through email to TA). 10% penalty for missing hardcopy or softcopy.
- More than 8 absences of class will get F grade
- To start class on time, late attendance is considered as 1/3 absence.
- Hint: many questions of exams are from the homework.
- Note: 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 강의평가
- "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
- "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."
Syllubus
This class covers automated software verification/testing techniques. The goal of the class is to learn practical applications of advanced verification/testing techniques, not sophiscated 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
Course Schedule
Sep 3 : Introduction
Sep 5: Necessity for systematic & automated testing techniques
Part I: Coverage criteria
Sep 10: Graph coverage (see Intro to Software Testing web sige)
Sep 12,24: Graph coverage for source code (see Understand C++ )
Sep 26: Logic coverage
Oct 1: CLang tutorial to build a branch coverage measuring tool
Oct 8: Logic coverage from source code
Oct 10: Category partitioning method (blackbox testing technique)
Part II: Software model checking
Oct 15,17:SAT-based bounded software model checking
Oct 22: Software model checking examples
Oct 24: 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
Oct 29:SAT solver heuristics, Using SAT solver for Sudoku
- "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
Oct 31: Midterm Exam
Part III: Logic model checking
Nov 7: Model checker SPIN part I
Nov 12: Model checker SPIN part II
Nov 19:Linear Temporal Logic
- Principles of the Spin Model Checker by M.Ben-Ari published by Springer
Part IV: Concolic testing
Nov 21: Automated SW analysis for high reliability: a Concolic testing approach
Nov 26: CREST Tutorial
Nov 28: CREST Examples, Busybox application examples through CREST-BV
Dec 3: Industrial Application of Concolic Testing on Embedded Software: Case Studies [ICSE'12 paper]
Dec 5: Automated Unit Testing of Large Industrial Embedded Software using Concolic Testing [ASE'13 paper]
Dec 10 :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 12: Examples of First Order Theories, SMTlib tutorial,
Dec 17: Final exam
Homeworks
- You need to submit both a hard copy and a soft copy for each homework.
- Report box for a hard copy: report box #392, 4th floor, N1 building
- Email address for a soft copy: send your soft copy to TA (yongbae2@gmail.com) via email.
- Please put [CS453] at the beginning of the title (ex. [CS453] Homework #1)
- HW1 : due Oct 1st 23:59
- HW2: due Oct 10 23:59
- Sample program: Sample.zip
- Tamplate: Tamplate.zip, grep.c
- Example code: Example.c, Example2.c
- HW3: due Oct 22 23:59
- HW#4: due Oct 31 23:59
- HW#5: due Nov 17 23:59 (due date is postponed)
- HW#6: due Nov 26 23:59
- HW#7: due Dec 6 23:59
- grep_1.2_v0.zip
- Martin Heisterman achieved the highest gcov branch coverage (53.69%) in HW7.
- HW#8: due Dec 17 23:59
- More explanation on formulation of a circuit in UF (see pages 10-15): Equality and Uninterpreted Functions
- Extra HW (optional 300 pts, delayed HW will not be accepted): due Dec 24 23:59
- Do the HW#7 question 2 with the goal to improve the gcov branch coverage of grep.c higher than 60%
- You should provide all answers for the 5 sub-questions
- If you achieve higher than 50% of the gcov branch coverage, you can get 200 pts
- If you already achieve more than 50%, just send an e-mail to TA to get 200 pts free.
- If you achieve higher than 40% of the gcov branch coverage, you can get 100 pts
- If you already achieve more than 40%, just send an e-mail to TA to get 100 pts free.