Personal tools
You are here: Home › Courses › CS655 System Modeling and Analysis, Fall 08

CS655 System Modeling and Analysis, Fall 08

Announcement

  • Sep 1st
    • the first class starts on Sep 2nd
    • No classes on Sep 16th and 18th due to Automated Software Engineering 08
  • Sep 2nd: CS655 BBS  is open
  • Sep 25th: We will have a supplementary class on Sep 30

  • Sep 30th: No class on Sep 30
  • Oct 28th: Midterm Exam on Nov 13th 4:00 PM - 6:00 PM
  • Oct 30th: HW#2 due Nov 11th
  • Nov 11th
    • Reading paper list is uploaded (updated with assignment information).
    • No class on Dec 2nd and Dec 4th due to APSEC 2008
  • Nov 20th: HW#3 "Specification & Verification of the Ricart-Agrawala algorithm" - due Dec 11th
  • Nov 28th:
    • If you have a trouble to play your presentation video clip, install AVC codec and then try it again. Windows media player 11 and Kmplayer worked fine.   

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-869-3543

E-mail: moonzoo@cs.kaist.ac.kr

Office hour: Tues & Thr 17:30-18:30

(reservation e-mail would be preferred)

  • Teaching assistants:

Changki Hong

Office: 2438 (located at the east wing)

E-mail:  kornin83@gmail.com

Phone: 042-869-3583

Office hour: Wed 4:00-7:00 PM

(reservation e-mail would be preferred)

  • Lecture hours: Tue & Thur 16:00 PM - 17:30 PM
  • Lecture room: 2443 (a.k.a the 3rd lecture room)
  • Prerequisite: CS204 Discrete mathematics
  • Grading: HW (3~4 times): 40%, Midterm exam: 30%, Seminar presentation:30%
    • Late HW is accepted with 20% penalty in 1 day, 40% penalty in 3 days. HW will not be accepted after that.
  • Note: The official language in the class is English. All students should submit homeworks in English.

Syllubus

  • Background
    As more and more computing systems are deployed as embedded systems in our daily life, the correctness of these systems are becoming crucial issue. Unfortunately, current status of research on design and analysis of such systems is not mature enough for realizing ubiquitous computing without risk. Formal modeling and analysis techniques can increase the reliability of computing systems with rigorous modeling and (semi)exhaustive analysis. This class focuses on practical application of formal modeling and analysis techniques for software systems.
  • Topics covered during
    First, we will cover model-oriented approach as a starting point. We will handle Calculus of Communicating Systems (CCS), NuSMV, and Promela for this purpose. Process algebra CCS has its advantage in concise syntax and clear semantics and serves as a basic framework of formal verification. In contrast, Promela is a comparatively rich language similar to C. Thus, Promela is more suitable to modeling real systems.  NuSMV is in between them.  Finally, we will study currently available code-oriented approaches such as CBMC and BLAST.  In these frameworks, a key is how to extract a formal from a complex code through sound abstraction. 
  • For the purpose of the class, this class involves intensive modeling and analysis practice based on the open source tools.

Course Material

Course Schedule

Wk 1~4 (Sep 2 ~ Sep 30) : Process algebraic approach - CCS and concurrent workbench

Sep 2: Orientation of the class

Sep 4: Intro. to Process Algebra

Sep 9: Formal Semantics of CCS

Sep 11: Examples of CCS models

Sep 23: Equivalence Semantics of CCS

Sep 25: Case study of multiple reader/writer system

Sep 30: Equivalence hierarchy

Oct 7: Algebra of Communicating Shared Resource (ACSR)

           Linear Temporal Logic

Oct 9th: Computational Tree Logic

Oct 14th: Model checking- NuSMV (1/2)

Oct 16th: Model checking- NuSMV (2/2)

Oct 28th: Model checking- Spin (1/3), Spin (2/3)

Oct 30th: Spin - advanced features

Nov 4th: SAT-based C program analysis, Algorithm for SAT

Nov 6th: Case studies - comparison of various model checkers

               - "Formal Verification of a Flash Memory Device Driver - an Experience Report" (Spin '08)

Nov 11th:"Unit Testing of Flash Memory Device Driver through a SAT-based Model Checker" (Automated Software Engineering '08)

Nov 13th: Midterm Exam

Nov 18th: PVS (prototype verification system) by Dr. Taeho Kim @ ETRI

Nov 20th:

Nov 25th:

Nov 27th:

Dec 9th:

Dec 11th:

Dec 16th:

Dec 18th:

Document Actions