Personal tools
You are here: Home › Courses › CS750B Special Topic : Formal Verification, Fall 06

CS750B Special Topic : Formal Verification, Fall 06

Administrative Information

  • Instructor : Moonzoo Kim
  • Lecture hour : Tuesday and Thursday 10:30 AM - Noon
  • Office hour : Tuesday and Thursday 1:30 PM - 3:00 PM
  • Classroom : 3444
  • Grade policy:
    • Seminar presentations (2 times) 50% (talk should be given in English)
    • Midterm exam : 30%
    • Homework (2~3 times) : 20%
  • Prerequisite: CS322 Formal language and automata
  • Note :  The official language of this class is 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 formal nature of computing systems is not mature enough for realizing ubiquitous computing without risk. Formal verification can increase the reliability of computing systems with rigorous modeling and complete verification. This class focuses on application of formal verification for software systems.
  • Topics covered during the first half of the class
    First, we will cover model-oriented approach as a starting point. We will handle Calculus of Communicating Systems (CCS) 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.
  • Topics covered during the second half of the class
    Then, we will study currently available code-oriented approaches such as BLAST and Java Pathfinder. In these frameworks, a key is how to extract a formal from a complex code through sound abstraction. In addition, we study the Esterel framework which generates C codes from a correctness-proven formal model. Thus, it can serve as a total framework from design to implementation, but with limited expressiveness.

Course Schedule

  • Wk 1~3 (Sep 5 ~ Sep 21) : Process algebraic approach - CCS and concurrent workbench
  • Wk 4~6 (Sep 26 ~ Oct 12) : Programming language modeling approach - Promela and SPIN
  • wk 7 (Oct 17 ~ Oct 19): Q&A session and mid-term exam
  • wk 8~13 (Oct 24~ Nov 30): Code-based verification frameworks
  • wk 14~15 (Dec 5 ~ Dec 14): (optional)Esterel - WYPWYE framework (What You Prove is What You Execute)

Reading Materials

Main texts of the class are published papers. Realindg list will be announced soon. In addition,

 

 

Lecture Slides

Document Actions