[an error occurred while processing this directive]

Computer-Aided Verification

Department of Computer Science and Information Engineering
National Chung Cheng University, Taiwan

Syllabus

Course Introduction Slides for Spring 2006 (PDF, 275 KB)

Reference Book || Course Contents || Background Requirements || Deadlines and Grading || Project Topics

Reference Book

Model Checking, Edmund M. Clarke, Jr., Orna Grumberg, Doron A. Peled, MIT Press, 1999.
(you can find it in the CCU library)
Top

Course Contents

Both the theoretical concepts and the practical use of Computer Aided Verification will be discussed.
  • Theory: Formal System Models, Specification Logics, and Model Checking Algorithms
  • Practice: Use of Verification Tools for verifying protocols, real-time systems, embedded software, and System-on-Chip (SoC).

PartsWeeks
Introduction to CAV1, 2
Introduction to Model Checking3
System Model and Logic Specification4, 5
Explicit/Symbolic Model Checking6, 7, 8
Mid-Term Exam9
BMC, SAT10
Assume-Guarantee Reasoning11, 12
Priority and Urgency Verification13
Coverage Analysis14
Paper Presentations15
Project Results Presentations16
Final Exam17
Top

Background Requirements

The only requirement is
  • software programming knowledge, at least the C programming language

The following are recommended but NOT required!

  • graph theory
  • automata theory
  • logic theory
  • computer architecture
  • software engineering

Top

Deadlines and Grading

WorkDeadlineGrade (%)
Labs & Assignments2 weeks due25%
Project ProposalMarch 29, 2006N/A
Project WorkApril, May 2006N/A
Paper SelectionApril 19, 2006N/A
Mid-Term ExamApril 19, 200620%
Paper PresentationJune 7, 200615%
Project Results Report and PresentationJune 14, 200620%
Final ExamJune 21, 200620%

Top

Project Topics

  • Verify a communication protocol (Bluetooth, 802.11, ATM, WAP, etc.)
    • Protocol modeled by extended timed automata (ETA)
    • Protocol requirements specified in CTL
    • Verification results
  • Verify a piece of real-time embedded software (RTES)
    • Software and hardware modeled by ETA
    • RTES requirements specified in CTL
    • Verification results
  • Verify a System-on-a-Chip (SoC)
    • SoC modeled by ETA
    • SoC design requirements specified in CTL
    • Verification results
  • Develop & Implement your own state-space reduction technique (BONUS: 40%)
    • Algorithm for your reduction technique
    • Proof of correctness for your algorithm
    • Implementation of your algorithm in SGM
    • Application examples
    • Reduction results
  • Develop a counterexample graphical viewer (signal timing diagram, MSC, UML sequence diagram, ...) (BONUS: 40%)
    • Representation modeling (how is a counterexample represented by your selected view from above)
    • Proof of equivalence (counterexample == represented view)
    • Implementation in SGM
    • Application examples
  • Develop an interface in SGM for Safecharts (BONUS: 50%)
    • Input syntax for Safecharts
    • Semantics storing for Safecharts
    • Translation from Safecharts to extended timed automata
  • Develop an interface in SGM for UML State Machines (formerly called Statecharts) (BONUS: 40%)
    • Input syntax for State Machines
    • Semantics storing for State Machines
    • Translation from State Machines to extended timed automata
Top