Course Syllabus

Advanced Software Engineering
   - Introduction to Model Checking Theories and Tools  

BASIC INFORMATION

Instructor:        JUNBEOM YOO
Office:              New Millennium Bldg. Room 904
Office Phone:     02-450-3258
E-Mail:             jbyoo@konkuk.ac.kr
Homepage:        http://dslab.konkuk.ac.kr
Course Page:     http://dslab.konkuk.ac.kr/Class/2014/14ASE/14ASE.htm
 

DESCRIPTION

This course introduces fundamental theories underlying formal methods. It practices several formal methods through term projects. At the end of the semester, each student proposes a new research plan. This semester, especially, will focus on timed automata and UPPAAL - the famous model checker for timed automata.

COURSE ORGANIZATION

All students make several presentations of selected papers and their extended/related ones. At the end of the class, each student makes a proposal for future research plans.

COURSE OBJECTIVE

   - Understand fundamental theories underlying formal methods
   - Term Project
      - Timed Automata &  UPPAAL or TIMES
      - SMV & SPIN
   - Make a research proposal

COURSE TOPICS

1.     Introduction to Formal Methods (Theory)

2.     Practices for Formal Methods

A.  UPPAAL

B. SMV

C. SPIN

TEXT

1.     Required Text: “System and Software Verification” by B.Bérard, et. al., Springer

GRADING PLAN

1.     Attendance        0%

2.     Proposal           30%

3.     Presentations     70%