授课教师:   Dr. Song Xiaoyu, Portland State University
课程名称：   软硬件系统的形式化验证技术
教材名称:   Model checking, E. Clark, MIT Press
必备知识:   (Prerequisite) 离散数学, 算法
时间地点：上午：8：00－12：00   下午：14：30－18：30
6月15日：上午三教102   下午三教102
      6月16日：上午三教107   下午三教107
      6月18日：上午三教107   下午三教102
      6月19日：上午三教106   下午三教107
授课教师背景：宋晓宇教授1984年毕业于国防科技大学计算机系，获学士学位；1991年毕业于意大利比萨大学计算机科学系,获博士学位。1992年任加拿大蒙特利尔大学计算机科学系助理教授；1997年任加拿大蒙特利尔大学计算机科学系终身副教授；1998年任美国加州格登斯公司 (Cadence) 高级咨询工程师；现任美国俄勒冈波特兰州立大学电子工程系终身正教授。宋晓宇教授的研究方向是：形式化描述及验证，组合优化及算法,计算机辅助软件设计，数字及计算机系统。宋晓宇教授长期从事形式化验证，计算机辅助设计软件算法和理论的研究及开发，先后在相关国际学术[屏蔽]上发表100多篇学术文章，近5年内他的论文被SCI和EI收录近60篇。宋晓宇教授是多种学术[屏蔽]的编委和学术组织重要成员，多个国际学术会议的筹备委员，曾先后获意大利教育部, 瑞士世界实验室, 加拿大及美国多种优秀研究奖。
课程简介：随着系统复杂性的增加，设计出错的可能性也正在增加。在此, 关键性的问题是所得到的系统可以是数字系统、应用软件和操作系统软件等的一个混合体。这样的复杂系统必须满足符合原始的产品性能说明和安全约束的需求。在系统设计过程中, 由于顶层说明的定义是人工的，并且综合设计的细化过程通常需要人工的精细调整才能达到更高的性能，所以有必要保证中间设计步骤与用户说明的特性的一致性和正确性。成功的设计方法要求验证设计是设计过程的必需部分，而不是可有可无的。对于一个嵌入式系统，花费在验证设计上的时间是花费在设计上时间的80%。设计验证是任何重大系统开发过程面临的主要挑战。
虽然传统的模拟技术仍被用于验证设计，但是越来越复杂的设计使得该技术创建足够多的向量集变得很困难，甚至是不可能。所以，需要一种新的验证方法来应付这种情况。模型检验是一种用于验证有限状态并发系统的自动技术。它比基于仿真、测试和演绎推理的传统技术有许多优势。这种方法在实际中已经成功地用于验证复杂的数字系统设计和通信协议。在美国的大型IT公司中, 形式化验证技术已经成为保证系统正确性的一种强有力的方法。
本课程将介绍形式化验证技术的基本方法及原理。通过参加本课的学习, 可以对系统功能的模型的建立, 系统行为描述有更深的理解。本课程的内容是从事信息产业人材的必备基础.
The objective of the course is to introduce the participants to the practical formal verification techniques for system designs. Topics to be covered include: system modeling, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), formal specifications, CTL and LTL model checking, BDDs, symbolic verification, applications of theorem proving systems. Exercises are provided in the class.

课程具体安排：
第 1次课 (Thurday Morning)
内容提要:
Introduction to verification technology, Understand the basic notions of correctness, verification criteria, backgrounds. Design process, problems, Requirements of verification, Limitations of testing, Main approaches to formal specification and verification, an overview: specification, FSM-based model checking, theorem proving, etc.
教学重点与难点:
Concepts of formal specification and verification
Difference between verification and testing
讨论：
How the formal analysis is useful?
作业：
Small report on the state of the art is required.

第2次课 (Thursday afternoon)
内容提要:
Introduction to formal logics. Understand the basic notions for logics, proofs, specifications. Formal Logic & proof, What is a formal logic? Basic Notions: Interpretations, validity, satisfiability, inference, Proof process- Formal logics (a) Propositional logic; (b) First-order logic; Syntax (terms, formulas, normal forms, substitution), semantics, decidability (c) Higher-order logic, Tradeoffs: expressivity ? decidability.
教学重点与难点:
Difference between semantics and syntactic objects, Proof, Validity and Satisfiablity
Difference between formal logics.
讨论：
How the formal logic is useful?
作业：
More than 5 exercises are provided.

第3 次课 (Friday Morning)
内容提要:
System modeling, Understand the importance of system modeling and specification. Understand the basic notions for different characteristics of systems. Capture System characteristics Different modeling techniques, System specification and properties, Criteria for a good representation for systems.
教学重点与难点:
Characterize the system behaviors, Basic existing methodologies, Understand the system properties.
作业：
Two exercises are provided.

第 4 次课 (Friday afternoon)
内容提要:
Temporal logics, Understand the basic notions of temporal logics, Use temporal logics to specify the system behaviors. Semantic and syntax of a temporal logic, Linear and branching temporal operators, LTL, CTL
教学重点与难点:
Linear Temporal Logics, Computational Tree Logics, CTL syntactic constraints.
作业：
A set of exercises is provided。

第 5 次课 (Monday Morning)
内容提要:
Temporal Logic and Modeling Checking, Understand the extension of CTL, CTL*, Syntax and Semantics of CTL*, Power Expressiveness of CTL, LTL, CTL*Modeling Checking Problems, Algorithms for CTL Modeling Checking
教学重点与难点:
Comparison of Power Expressiveness of CTL, LTL, CTL*, Modeling Checking Problems
Algorithms for CTL Modeling Checking
作业：
Some problems are provided.


第6 次课 (Monday Afternoon)
内容提要:
Modeling Checking with fixpoint computation, Lattice notions, Fixpoint Theory, Fixpoint Characteristics for temporal operators, Modeling Checking algorithms with fixpoint computation
教学重点与难点:
Fixpoint Theory, Fixpoint Characteristics for temporal operators, Modeling Checking algorithms with fixpoint computation
作业：
Two questions are provided

第 7 次课 (Tuesday Morning)
内容提要:
Boolean Representations, Find a canonical Boolean representation, Binary Decision Diagrams (BDDs), Represent sets and set operations by BDDs, Node ordering, Represent sets and set operations by BDDs
- A canonical representation of Boolean functions and relations
- Variable ordering and heuristics
- Logic operations
- Representing state transition functions, relations and sets of states
教学重点与难点:
Boolean representations
Binary Decision Diagrams (BDDs)
Represent sets and set operations by BDDs
作业：
Two questions are provided

第 8 次课 (Tuesday Afternoon)
内容提要:
Symbolic verification based on BDD and SAT, Symbolic representations, Symbolic model checking, Symbolic Simulation, Implicit reachability analysis, FSM Equivalence checking
教学重点与难点:
Symbolic State Enumeration with Fixpoint Characteristics, Symbolic model checking algorithms, SAT-based model checking
作业：
One problem is provided

第 9 次课 (Wednesday Morning)
内容提要:
Theorem Proving systems, Overview of available theorem proving systems, Basic theory for proving systems, Using logic to specify and verify a design showing how to: a) Specify structure of the design b) Specify the intended behavior / properties c) Specify input restrictions and relation to satisfy d) Step-by-step proof example  
教学重点与难点:
Computer-assisted formal proof, Proof checker, Automated deduction systems for a decidable subset; Interactive Theorem Proving.
作业：
A question is provided.

第 10 次课 (Wednesday Afternoon)
内容提要:
LTL Model Checking and Buchi Automata, abstract state enumeration, Language containment methods, Omega- automata, LTL modeling checking, Abstract state enumeration
Language containment methods
教学重点与难点:
Omega- automata, LTL modeling checking, Abstract state enumeration with non-interpreted function symbols
讨论：
The difference between language containments, with CTL model checking
作业：
A report is required.