Personal tools
You are here: Home › Courses › CS453 Automated SW Testing, Fall 15

CS453 Automated Software Testing, Fall 15

Announcement

  • Aug 31: The first class starts on Sept 1 
  • Sep 22: No class on Sep 29 due to temporarily designated national holiday
  • Sep 24: Linux account will be given to every student to do programming HWs.  See Noah BBS for detail. 
  • Sep 24: "Overview on testing techniques" on Sep 8 is updated to include the input partitioning technique which is useful for HW#2.
  • Sep 26: Please ask all questions on Noah BBS so that other students can share Q&A  and reduce the work of TAs to answer the same questions multiple times.
  • Oct 5: HW#3 is slightly updated to get a regular C file as an input without preprocessing.
  • Oct 12: Q3 and Q4 of HW#3 are  slightly updated to receive a preprocessed C file to avoid difficulty of updating macros.  See the updated HW#3.
  • Oct 13: No class for Nov 10 and 12 due to Automated Software Engineering (ASE) conference
    • Make-up class: Oct 16 (Fri) 7:00 - 9:30 PM 
  • Oct 28: No class for Dec 8 and 10 due to ICSE 2016 Program Board meeting
    • Make-up class: Dec 4 (Fri) 7:00 - 9:30 PM

Administrative Information

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: Tue/Thur 10:30 AM-12:00  

(reservation e-mail would be preferred)

  • Teaching assistants: Choongwoo Han (cwhan.tunz at gmail.com, x7743), Ji-Hoon Kim (june1116 at kaist.ac.kr, x7747)
  • 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. 
    • 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.
    • All programming HWs you submit must be able to replayed by executing a single script file on a TA's verifier account (i.e., submitted HW should not have  dependency on your home directory, environment, etc.).  Also, the replayed execution must demonstrate the same output to the submitted hardcopy. You will get 10% penalty of the max score otherwise.
      • For your programming HWs, you should not use external libraries which are not available on the verifier machines.  If you really need an external library, you have to ask TAs to install it on the verifier machines.  
    • More than 7 absences of class will get F grade
      • To start early morning class on time, late attendance shall be considered as 1/3 absence. 
      • No excuse for the absence of class except grad students who are occupied by his/her lab activities (e.g., attending conf, etc.) with 1 week prior notice.  
  • The official language in the class is English. All students should submit all written documents such as homeworks, project reports, exams, etc. in English; 10% penalty of the max score otherwise.
  • Questions and answers can be done through Noah BBS
  • Excerpts from 강의평가
    • "실질적으로 써먹을 수 있는 내용을 많이 배워서 보람찼습니다"
    • "과제가 많이 어려운것 같았다. 과제에 대한 도움을 수업에서 좀 더 주었으면 좋겠다."

Syllabus

 This class covers automated software verification/testing techniques to fight the high complexity of software. 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 guides students to utilize various software verification/testing tools and learn the underlying mechanisms to produce verification results for the target software effectively and efficiently.

Course Material

Course Schedule

Sep 1 : Introduction

Sep 3: Necessity for systematic & automated testing techniques

Part I: Program coverage criteria and program analysis tools

Sep 8: Overview on testing techniques (including the input partitioning technique)

Sep 10,15: Graph coverage 

Sep 17: Graph coverage for source code 

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

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

Sep Oct 1: Logic coverage

Oct 6, 8:  Logic coverage from source code 

Oct 15: LLVM IR tutorial 

  • getelementptf : FAQ

Oct 17: Clang v.s. LLVM

Oct 20 : Mid-term exam (9:00- 11:00 AM)

Oct 27: LLVM Pass tutorial 

 

Part II: Model checking

Oct 29:SAT-based bounded software model checking

Nov 3: Software model checking examples 1 

Nov  5, 17: Model Checking flash memory storage platform software - an industrial case study

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

Nov 24:  Model checker SPIN part I

Nov 26: Model checker SPIN part II

 

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

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

Dec 1: CREST Tutorial, CREST Examples,

Dec 3: Busybox application examples through CREST-BV,  Automated Unit Testing of Large Industrial Embedded Software using Concolic Testing  [ASE'13 paper] 

Dec 4: First order theories, SMTlib tutorial,

Dec 15: Final exam (9:00-11:00 AM)

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 (#381), 4th floor, N1
    • Email address for a soft copy: send your soft copy to both TAs via email  
      • 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 programming HWs.  See the class noah bbs for detail
    • ID: your student #, initial password: ID!!
      • You have to change your password when you log-in first time.
    • Note that your account will be deleted at the end of the semester.  Don't forget to backup your own data 
  • 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 22 (Tues) 23:59
    2. HW#2 (coverage guided testing, 100 points): due Oct 6 (Tues) 23:59
    3. HW#3 (source code branch coverage measuring tool using Clang, 200 points): due Oct 15 (Thurs) 23:59
    5. HW#5 (SAT-based bounded model checking C programs using CBMC, 100 points): due Nov 17 (Tues) 23:59
    6. HW# 6 (Model checking using Spin, 100 points): due Dec 3 (Thurs) 23:59
    7. HW#7 (Concolic testing, 350 points): due Dec 13 (Sun) 23:59
    Document Actions