Model Checking Lei Bu

大纲 为什么模型检验？ 什么是模型检验？ 怎么做模型检验？ 更高更快更强 复杂系统模型检验

计算机已经渗透到我们工作和生活的方方面面，极大地促进了社会的发展和生产力的提高。 工作在我们身边的各种计算机系统由于其中的软硬件系统失效经常表现不尽人意，甚至造成不可挽回的损失 随着计算机技术在各行各业应用的日益普及,计算机已经渗透到我们工作和生活的方方面面，成为我们工作和生活的一部分，从而极大地促进了社会的发展和生产力的提高。 与此同时，工作在我们身边的各种计算机系统由于其中的软件系统失效经常表现不尽人意，呈现出脆弱、难以信任的特征，甚至造成不可挽回的损失，因此研究相关的可信软件关键技术以提高软件系统的可信性已经成为十分迫切的需求。

硬件 奔腾芯片 93-94 60-100 MHz FDIV Bug：某数学家发现用一个数字去除以824,633,702,441时，答案一直错误 $500 million Intel内部统计 每设计一个新版本Bug数目增加4倍… 物价飙升… 奔腾四芯片 2000-2007 1.5GHz，4200万晶体管 8000 Bugs！

欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在 发射40秒后爆 炸，原因是惯 性参考系统 软件的数据 转换异常造 成的失效。

美国F-22猛禽战斗机 2004年12月20日，美空军第422测试评估大队的一架F-22战斗机因软件问题在起飞过程中失控坠毁。 2007年2月9 日同样因软 件问题延迟 在日本部署

我们的信息基础设施 正建立在脆弱的软硬件之上 我们的信息基础设施 正建立在脆弱的软硬件之上

提高系统可靠性 质量管理 在系统开发过程中加强管理，防止可能出现的错误。 测试（testing）或 仿真（simulation） 以运行系统（模型）为主要手段发现系统错误。 验证（Verification） 建立系统模型，确认系统模型是否存在错误。

提高可信度的途径 测试（testing）或 仿真（simulation） 无法回答系统一定没有错误这样一类问题 形式化验证（Formal Verification） 可以从某一个角度回答系统一定没有错误这样一类问题，从而进一步提高我们对系统可靠性的可信度

形式化方法 形式化方法包括： 形式验证包括： 形式化方法是指为说明和验证复杂计算机系统所采用的基于数学的语言、技术和工具。 规约（specification） 验证（verification） 形式验证包括： 定理证明（theorem proving） 模型检验（model checking）

模型检验 模型检验是一种自动验证有穷状态系统的技术。 模型检验的基本思想是通过遍历系统模型的状态空间来检验系统模型是否满足给定的性质。 模型检验技术的创始人（1981）： E.M. Clarke (CMU,US) E.A. Emerson (UT Austin, US) J. Sifakis (Verimag, France)

在硬件，协议设计上巨大成功 现有手段：测试、仿真 形式化方法 太多可能、慢、无法穷尽、没有保障 举例：加法器测试： 2 160 个浮点数对… 自动证明、确定性结果 奔4 浮点数计算部 牛刀小试： Can we do more？ 2003：FV found many high-quality bugs in P4 and verified “20%” of design FV is now standard practice in the floating-point domain 2009：Replacing Testing with Formal Verification in Intel  𝐂𝐨𝐫𝐞 𝐓𝐌  i7 Processor Execution Engine Validation @ CAV09

07 Turing Award!

模型检验的过程 建模（Modeling） 规约（Specification） 验证（Verification）

模型检验 在模型检验中涉及两种形式说明语言： 性质说明语言用于描述系统的性质; 模型描述语言用于描述系统的模型。 模型检验技术用于检验由模型描述语言描述的系统模型是否满足由性质说明语言描述的系统性质。

模型检验 OK Finite-state model or Error trace Model Checker Line 5: … Line 12: … Line 15:… Line 21:… Line 25:… Line 27:… … Line 41:… Line 47:… Finite-state model Model Checker (F W) Temporal logic formula

模型：Kripke Model Kripke Structure + Labeling Function S 有穷状态集合 Atomic Proposition，AP为原子命题集合. Kripke Model: M = (S, s0, R, L) S 有穷状态集合 s0S 初始状态 RS  S 状态迁移 L: S→2AP 状态上的成真命题

Kripke Structure

Temporal Logics Express properties of event orderings in time Branching Time Every moment has several successors Infinite tree Computation Tree Logic (CTL) Linear Time Every moment has a unique successor Infinite sequences (words) Linear Temporal Logic (LTL)

Path quantifiers and Temporal operators Path quantifiers: A ( for all computation path ) E ( for some computation path ) Temporal operators: X, F, G, U, R Software Engineering Group

X (next time) requires the property holds in the second state of the path F (eventually) the property will hold at some state on the path G (always) the property holds at every state on the path U (until) if there is a state on the path where the second property holds, at every preceding state, the first one holds R (release) the second property holds along the path up to and including the first state where the first property holds. However, the first property is not required to hold eventually

CTL ten basic CTL operators: AX and EX AF and EF AG and EG AU and EU AR and ER Software Engineering Group

Each of the ten operators can be expressed in terms of EX, EG and EU AX f= ! EX(!f) EF f= E[True U f] AG f =!EF(!f) AF f= !EG(!f) A[f U g]= !E[!gU(!f ^ !g)] ^ !EG !g A[f R g] = !E[!f U !g] E[f R g] = !A[!f U !g]

CTL Software Engineering Group

Examples Let "P" mean "I like chocolate" and Q mean "It's warm outside." AG.P "I will like chocolate from now on, no matter what happens.“ EF.P "It's possible I may like chocolate some day, at least for one day." AF.EG.P "It's always possible (AF) that I will suddenly start liking chocolate for the rest of time." (Note: not just the rest of my life, since my life is finite, while G is infinite). EG.AF.P "This is a critical time in my life. Depending on what happens next (E), it's possible that for the rest of time (G), there will always be some time in the future (AF) when I will like chocolate. However, if the wrong thing happens next, then all bets are off and there's no guarantee about whether I'll ever like chocolate." Software Engineering Group

A(PUQ) "From now until it's warm outside, I will like chocolate every single day. Once it's warm outside, all bets are off as to whether I'll like chocolate anymore. Oh, and it's guaranteed to be warm outside eventually, even if only for a single day." E((EX.P)U(AG.Q)) "It's possible that: there will eventually come a time when it will be warm forever (AG.Q) and that before that time there will always be some way to get me to like chocolate the next day (EX.P)." Software Engineering Group

Express Properties Safety: something bad will not happen Typical examples: AG ( reactor_temp > 1000 ) Usually: AG Software Engineering Group

Express Properties Liveness: something good will happen Typical examples: AF( rich ) AF( x > 5 ) AG( start -> AF terminate ) Usually: AF Software Engineering Group

Express Properties Fairness: something is successful/allocated infinitely often. Typical examples: AGAF ( enabled ) Usually: AGAF Software Engineering Group

基本验证方法 自动枚举、遍历所有状态 为每个状态标记其满足的性质 找出标记了目标规约f的状态集 所有初始状态都在此集合中？

First find all states labeled with Work backwards, find all states that can be reached by a path in which each state is labeled with All such states should be labeled with g.

Base on nontrivial strong connected components. Nontrivial: has more than one or contain one node with a self-loop.

LTL M |= p if (M): M, |= p Semantics M,  |= Op if M, 1 |= p M,  |= p if i≥0: M, i |= p M,  |= []p if i≥0: M, i |= p M,  |= pUq if i≥0: M, i |= q and j<i: M, j |= p M,  |= pRq if i≥0: M, i |= q or i≥0: M, i |= p and j≤i: M, j |= q M |= p if (M): M, |= p

LTL p []p pUq pRq p p p... p q q q,p

Büchi Automata Automaton which accepts infinite traces A Büchi automaton is 5-tuple , S, I, , F  is a finite alphabet S is a finite set of states I S is a set of initial states   S   S is a transition relation F S is a set of accepting states An infinite sequence of states is accepted iff it contains accepting states infinitely often

Example 1=S0S1S2S2S2S2… 2=S0S1S2S1S2S1… 3=S0S1S2S1S1S1… b a,d a S0 c S2 d 1=S0S1S2S2S2S2… ACCEPTED 2=S0S1S2S1S2S1… ACCEPTED 3=S0S1S2S1S1S1… REJECTED

LTL Model Checking Given a model M and an LTL formula  Build the Buchi automaton B¬ Compute product of M and B¬ The product accepts the traces of M that are also traces of B¬ (M  ¬) If the product accepts any sequence We have found a counterexample

关键问题 安全性问题 可达性问题 模型检验中的关键技术问题 如何设计数据结构和算法，用以表示和遍历大规模的系统模型状态空间。 安全性问题 可达性问题 模型检验中的关键技术问题 如何设计数据结构和算法，用以表示和遍历大规模的系统模型状态空间。 解决由多个系统模型的并行组合而形成的状态空间爆炸问题。

Symbolic Model Checking 用布尔公式刻画状态集合和状态对集合, 用 Ordered Binary Decision Diagram（OBDD）来表示这些布尔公式, 使用OBDD上的布尔操作来计算谓词转换子,从而使模型检验在压缩了的符号化状态空间上来验证CTL性质 a,b a,!b

Ordered Binary Decision Diagram (OBDD) 1 b1 b1 1 1 a2 a2 a2 a2 1 1 1 1 b2 b2 b2 b2 b2 b2 b2 b2 1 1 1 1 1 1 1 1 1 1 1 1 (a1  b1)  (a2  b2)

Reduced Ordered BDD a1 1 b1 b1 1 1 a2 a2 a2 1 1 1 b2 b2 b2 b2 b2 b2 1 b1 b1 1 1 a2 a2 a2 1 1 1 b2 b2 b2 b2 b2 b2 1 1 1 1 1 1 1 1 1 1 (a1  b1)  (a2  b2)

Reduced Ordered BDD a1 1 b1 b1 1 1 a2 a2 1 1 b2 b2 b2 b2 1 1 1 1 1 1 1 b1 b1 1 1 a2 a2 1 1 b2 b2 b2 b2 1 1 1 1 1 1 1 1 (a1  b1)  (a2  b2)

Reduced Ordered BDD a1 1 b1 b1 1 1 a2 1 b2 b2 1 1 1 1 b1 b1 1 1 a2 1 b2 b2 1 1 1 1 (a1  b1)  (a2  b2)

Reduced Ordered BDD a1 1 b1 b1 1 1 a2 1 b2 b2 1 1 1 b1 b1 1 1 a2 1 b2 b2 1 1 1 (a1  b1)  (a2  b2)

主要优化技术 On-the-fly技术 对称技术（Symmetry） 偏序规约技术（Partial order reduction） 反例制导的抽象精化（Counterexample Guided Abstraction Refinement, CEGAR）

On the fly Symmetry Reduction 把状态空间生成和检验它是否满足性质合在一起做，而不去预先生成整个状态空间，从而尽可能避免状态爆炸。 Symmetry Reduction 针对由多个完全类似的进程组成的系统，利用其模型的状态空间的对称性来生成压缩的且对模型检验等价的模型

Partial Order Reduction 通过发掘系统中并发执行的迁移的交换性,减少本质上相同的状态,从而仅生成足以检验性质的小部分状态空间 s s a b a s1 s2 s1 b a b r r No Reductions States Reduced

反例制导的抽象精化 I MUST ABSTRACT!! Too many states to handle ! = bad state

抽象（Abstraction） 通过抽象来减化模型 可能带来误报或漏报 不规则状态规则化 具体值集合化 。。。 x:int Even Odd …, -2, 0, 2, 4, … x:int …, -3, -1, 1, 3, …

Counterexample-Guided Abstraction-Refinement (CEGAR) Build New Abstract Model Model Check M M’ Pass No Bug Fail Check Counterexample Obtain Refinement Cue Spurious CE Real CE Bug

有界模型检验 Bounded Model Checking (BMC) A.I. Planning problems: can we reach a desired state in k steps? Verification of safety properties: can we find a bad state in k steps? Verification: can we find a counterexample in k steps ?

SATisfying assignment! If there exists an assignment to Boolean variables that makes the formula true？ literals 1 = (b c) 2 = (a d) 3 = (b d)  = 1 2 3 A = {a=0, b=1, c=0, d=1} clauses SATisfying assignment!

经典的SAT－Based BMC 方法 输入: 模型 M, 时序公式f, and 用户制定步长k 构建命题公式W(k) ，此命题公式成真，satisfiable， 当且仅当 f 在某个长度为 k的路径上满足。 长度为k的路径: 假设 f = EF p ，k = 2, AG p呢？

BMC idea (cont’d) AG p means p must hold in every state along any path of length k We take That means we look for counterexamples

Safety-checking as BMC p is preserved up to k-th transition iff W(k) is unsatisfiable: . . . s0 s1 s2 sk-1 sk p p If satisfiable, satisfying assignment gives counterexample to the safety property.

Example: a two bit counter Initial state: 00 01 10 11 Transition: Safety property: AG W(2) is unsatisfiable. W(3) is satisfiable.

SMT based BMC SAT SMT 纯布尔命题逻辑 无法处理更复杂问题… 无量词一阶逻辑 除了布尔命题，还可处理复杂约束如3x+2y-z>4， sin(x)/y>m+n等 命题逻辑处理简单的陈述性命题，一阶逻辑补充覆盖了谓词和量化 While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification

复杂系统模型检验 实时嵌入式系统 信息物理融合系统 物联网 软件代码

实时嵌入式系统 嵌入式系统 反应式系统 实时系统 混成系统 特定应用、嵌入到对象系统中 接受外界输入、作出反应、持续交互 严格的时间约束、在给定时间间隔内给出响应 混成系统 离散化逻辑控制、连续性时间行为

水箱监控系统 水箱的水位在什么区间？ 初始状态时，水箱中水面的高度为1英寸； 水泵打开时，水箱中水面以每秒1英寸的速度上升； 水泵关闭时，水箱中水面以每秒2英寸的速度下降； 水位达到10英寸时，监控器发出关闭水泵信号，5英寸时发出打开信号 监控器发出信号打开（关闭）水泵到实际打开（关闭）水泵之间有2秒钟的延迟； 水箱的水位在什么区间？

混成系统 有穷迁移系统，描述控制逻辑跳转 每个节点上有微分方程存在，描述相应实时行为

混成系统研究现状 研究现状及趋势 有界模型检验： 标准模型检验： 性能 性能 SMT Polyhedral Computation Interleaving Semantic 性能 低维度 低阈值 研究现状及趋势 标准模型检验： Polyhedral Computation Cartesian Product 性能 不可判定 低维度

我们的工作 单路径可达性检验 组合路径可达性检验 有界路径可达性检验 连续时间行为离散化抽象 线性编码并求解 深度优先遍历 逐条检验 基于共享事件的同步语义 线性编码并求解

工具现状 JAVA Application Web Service 公开发布，国际下载（CMU,UIUC,UCB,UBC…）

CPS Cyber-Physical System 动态环境、外界信号、大规模组合混成系统 安全攸关系统 需要验证！

示例系统一 南方某市在建CBTC列控系统 行为规约 列车与RBC频繁通信获取下一周期移动授权500ms. 行进至安全刹车点，正常制动. 5秒未收到信号，紧急制动 行为规约 运行过程中不可超出移动授权范围 前后车不会追尾

示例系统二 激光刀气管切开手术系统 行为规约 呼吸机向病人气管中泵入氧气 气管氧气浓度（ 𝑂 2 ）、体内血氧浓度（ 𝑆𝑝𝑂 2 ）监测器实时监控病人体征 (4秒一次) 行为规约 激光刀打开时气管中氧气浓度不可过高（点燃气管，每年各国均有大量相关致死案例报道） 手术中病人体内血氧浓度不能过低（窒息死亡）

建模与验证 经典模型检验问题 列车 列控方程中大量实时参数（如每周期移动授权具体值、实时风速、坡度等等 ），离线无法获取—>无法建模 大量非线性方程存在—>难以验证 手术 血氧浓度变化方程无法建模（医学难题） 原因：血氧浓度长期变化行为是一个异常复杂的生化反应系统，情绪变化都可引起相关参数剧烈波动 气管氧气浓度为非线性方程难以验证

在线建模与验证 关键参数实时数值捕获 (固定数值) （描述） 短期内可预知行为 （建模） 短期内可描述模型 （验证） 在线快速模型检验，验证系统安全 系统运行 控制方程 安全攸关关键 场景在线验证 控制参数 实时建模 信号接收 在线局部静态模型 实时参数 验证未通过 启动备案 参数采用

在线建模及试验评估 列控 病人 10车系统 109ms< 500ms 932ms <4 s 列控 病人 10车系统 109ms< 500ms 932ms <4 s （前值为多次验证时间平均值，后值为更新周期） 性能上满足要求！

当前主要方向 非线性实时系统验证 CPS系统验证与协同设计 用户级物联网验证与自动修复 软件代码验证

Thanks Q&A