FORMAL METHODS  (921 U7600)
Spring 2007

教師：王凡

每週二9：10 - 12：00

博理館103教室

Announcement

•  2008.03.04 ¤W¤Èªº½Ò§ó°Ê¦p¤U: 8¡G30-10¡G00,¦aÂI½Õ¨ì¸ê°T¨t216. §Ú­Ì±N°Ñ¥[¥xªk¬ì§Þ¥æ¬y·|ijÃö©óformal verificationªºsession. 10¡G30-12¡G00,«ì´_¨ì³Õ²zÀ]103.

Workout

•   Workout1: Lecture notes 4 - p39, p41, pp45-46 Due:2008/3/18

Class Notes (under revision constantly)

•  Syllabus

• Lecture notes 1, introduction 

• Lecture notes 2, propositional logics

•  Lecture notes 3, predicate logics

•  Lecture notes 4, state machines

• Lecture notes 5, temporal logics & model-checking

• Lecture notes 6, embedded systems

• Lecture notes 7, process algebrae

• Lecture notes 8, theorem proving and program correctness

• Lecture notes 9, Petri nets

• Lecture notes 10, VDM, Z, & B

• Lecture notes 11, UML

• Lecture notes 12, HDL

• Lecture notes 13, RED & UPPAAL

• Lecture notes 14, CUDD & SMV

• Lecture notes 15, Statemate & Rhapsody

Term Projects: (Due: 12/31/2002, absolute deadline)

• Project 1: Implementation of a SUDOKO logic solver with REDLIB (mid-presentation 2007/3/27, deadline 2007/4/10)
• Project 2: Implementation of weakest precondition construction (mid-presentation 2007/4/24, deadline 2007/5/8)
• Project 3: Implementation of a backward risk condition checker (mid-presentation 2007/5/22, deadline 2007/6/12)

 

Examinations

• Midterm (sample) 2007/04/24 with solutions
• Final (sample) 2007/06/26 with solutions

Papers to read and present on 2007/5/29, 2007/6/5, and 2007/6/12.

 

Additional course materials from the webs:

• Introduction: (1), (2), (intro.alur-henzinger)
• Automata Theory: (brief introduction) (2nd order theory of one successor)
• Temporal Logics:
• Linear time 1
• Branching time 1, 2
• Model Checking: -- a tutorial,
  (1), (2), (3), (CTL model checking), (fixed point), (Symbolic CTL model checking ) ( Survey on mu-calculus)
• Binary Decision Diagrams (BDD) ( Survey on BDD)
• Timed automata, Symbolic approach, Undecidability of multi-rate timed automata ---- (Surveys on Timed automata, Hybrid automata)
• State space explosion: Intro., Bisimulation, Partial order reduction
• Some infinite state systems: Petri nets ( 1, 2); communicating finite state machines
• Compositional Verification
• Probabilistic model checking
• Supervisory Control
• CAV Tools

• Verification examples: