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 30: 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
Instructor: Moonzoo Kim
- Office: 2434 (east wing)
- Phone: 042-869-3543
- E-mail: moonzoo@cs.kaist.ac.kr
- Office hour: Tues & Thu 17:30-18:30 (reservation e-mail preferred)
- Teaching assistants:
- Changki Hong — Office: 2438 (east wing) — E-mail: kornin83@gmail.com — Phone: 042-869-3583
- Lecture hours: Tue & Thu 16:00 - 17:30
- Lecture room: 2443 (3rd lecture room)
- Prerequisite: CS204 Discrete Mathematics
- Grading: HW (3–4 times) 40%, Midterm exam 30%, Seminar presentation 30%
- Late HW policy: 20% penalty in 1 day, 40% penalty in 3 days; HW not accepted after that.
- Note: The official language in the class is English. Submit homeworks in English.
Syllabus
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
Reading list (selected):
- Process Algebra by R. Cleaveland and S. A. Smolka
- Proving Testing Preorders for Process Algebra Descriptions by F. Corno et al.
- End-to-End deployment of Formal Methodology (case study) by M. Kim and I. Kang
- The Linear Time-Branching Time Spectrum I by R. J. van Glabbeek
- Logic in Computer Science (2nd ed) by M. Huth and M. Ryan
- The Model Checker Spin (Holzmann)
- A Tool for Checking ANSI-C Programs (CBMC)
Related tools / home pages:
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)
- 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 (CBMC), Algorithm for SAT
- Nov 6th: Case studies - comparison of various model checkers
- 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:
- Lazy Abstraction by T.A. Henzinger et al. POPL '02 (Yunho Kim)
- Zing: Exploiting Program Structure for Model Checking Concurrent Software by T. Andrews et al. CONCUR '04 (Changki Hong)
- Nov 25th:
- Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code by C. Killian et al. NSDI '07 (A.D. Quang)
- Model Checking Programs by W. Visser ASE '03 (Hyunik Na)
- Nov 27th:
- Thorough Static Analysis of Device Drivers by T. Ball et al. EuroSys '06 (Junghoon Park)
- CUTE: A Concolic Unit Testing Engine for C by K. Sen et al. FSE '05 (Anna Chen)
- Dec 9th:
- The Daikon system for dynamic detection of likely invariants by M.D. Ernst et al. Science of Computer Programming 69 (2007) (B. Chervet)
- The Software Model Checker Blast: Applications to Software Engineering by D. Beyer et al. STTT '07 (Yunho Kim)
- Dec 11th:
- Bounded Model Checking of Concurrent Programs by I. Rabinovitz and O. Grumberg, CAV 2005 (Changki Hong)
- Fair Stateless Model Checking by M. Musuvathi and S. Qadeer, PLDI 2008 (A.D. Quang Pham)
- Dec 16th:
- Dynamic Recognition of Synchronization Operations for Improved Data Race Detection by C. Tian et al., ISSTA 2008 (Hyunik Na)
- BLASTing Linux code by J.T. Mühlberg and G. Lüttgen, FMICS 2006 (Junghoon Park)
- Dec 18th:
- Automated Environment Generation for Software Model Checking by O. Tkachuk et al., ICSE 2003 (Anna Chen)
- Using Model Checking to Find Serious File System Errors by J. Yang et al., OSDI 2004 (B. Chervet)