1、领域模型与形式化验证技术领域模型与形式化验证技术 中兴通讯操作系统 李凯航 CONTENTS 01 形式化技术简介 1.1 定理证明 1.2 模型检测 1.3 LTL概念 02 怎样验证领域模型的正确性 2.1 用时态逻辑状态机表达模型 2.2 用不变式检查模型归纳性质 2.3 用线性时态逻辑检查模型正确性 2.4 Intel ACRN InterruptWindow模型正确性验证 03 怎样用形式化技术推导一个正确模型 3.1 理论方法 3.2 物联网操作系统内存管理模型设计推导 软件正确性如何保证？大家知道的方法 编码测试需求模型分析模型设计模型同行评审同行评审代码走查需求模型编码TDD用

2、例重构修正大家知道的方法 问题一：需求如何建模？图、表、语言、文字等更加感性的东西，能否表达清楚用户到底需要什么？问题二：需求分析到领域模型的正确性如何验证？传统的同行评审存在较大程度人为经验的因素，包括评审组人员的构成、背景、经验都会最终影响设计正确性的保证。需求实例化领域模型编码验收测试TDDDSL(BDD)修正修正我们的方法是什么我们的方法是什么 领域模型需求模型数学形式化模型数学形式化验证定理模型：代码模型领域模型需求模型数学形式化模型模型验证定理模型时态逻辑状态机模型不变式+时态属性求精形式化技术简介 形式化技术简介 由于传统的软件工程方法无法从根本上保证软件设计的安全性、正确性，因

3、此必须有一种客观性的理论方法来保证在需求分析、概念建模阶段就存在一个可量化、能够验证的模型才能从根本上解决上述问题，这种方法在目前业界叫做形式化方法，形式化方法的核心就是形式化语言，以及基于形式化语言构建出来的形式化模型。定理证明模型检测定理证明 基本原理是使用数理逻辑公式规格化描述目标系统模型、需要满足的性质，使用数理逻辑的公理、定理、推导规则结合系统模型的描述公式推导出系统需要满足的性质。系统模型定理推导系统性质模型正确X需要人工干预？X模型检测 将系统建模成有限状态系统，系统的性质用时态逻辑公式表示如：CTL，LTL等，在此模型上利用状态穷举计算来验证性质的正确性，模型检测与定理证明相比

4、有很大优势，可以全自动地验证，不需要人工干预，而定理证明则在一些关键推导路径中需要数学家控制，但是模型检测有可能会产生状态组合爆炸。系统模型系统性质全自动模型状态穷举计算模型正确XX状态组合爆炸？LTLLTL概念 线性时态逻辑是由命题时态逻辑（PTL）和一阶时态逻辑（FOTL）组成，其中PTL、FOTL本质上是在命题逻辑、一阶逻辑基础上扩展了模态词或时态算子的模态逻辑。always算子 -F表示F总是为真或者F永远为真 sometimes算子 -F表示F最终为真或者F有时为真 next算子 -F表示F在下一时刻为真 until算子 -F1 F2表示F1一直为真直到F2为真 线性时态逻辑所用到的

5、时态算子 LTLLTL概念 命题时态逻辑公式的BNF表示为：:=P|一阶时态逻辑公式的BNF表示为：:=P|x.|x.|PTL公式和FOTL公式统称为LTL公式 怎样验证领域模型的正确性 用时态逻辑状态机表达领域模型 一个现实中的例子：VT01用时态逻辑状态机表达领域模型 波形的变换符合下面规律：v=0-v=1-v=0-v=1.这是一个有规律变化的无穷序列 给了我们一个启发：能否用一个时序状态机模型来表达它？VT01用时态逻辑状态机表达领域模型 VT01用时态逻辑状态机表达领域模型 理解几个基本概念 Safety：表征一个系统不符合要求的事件一定不能发生 Liveness：表征一个系统符合要求

6、的事件最终一定要发生 时态逻辑状态机公式=Init/Safety/Liveness 用不变式检查模型归纳性质 题目：求两个自然数的最大公约数，验证欧几里德算法正确性 用不变式检查模型归纳性质 能保证算法是正确的吗？结果是正确的并不代表算法每一步都是对的，因此上面的不变式只能保证算法部分正确性。保证算法全局正确性的不变式需要满足可归纳性，数学公式必须满足：用不变式检查模型归纳性质 正确的不变式是什么？结论：不变式检查主要是针对可归纳性全局状态属性 用线性时态逻辑检查模型正确性 题目：求两个自然数的最大公约数，验证欧几里德算法正确性 用线性时态逻辑检查模型正确性 正确性属性需要考虑哪些因素？一个真

7、实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 ACRN背景简介：ACRN是Linux基金会今年发布的一款新的嵌入式hypervisor参考软件，项目的官方名称为ACRN，这是一个专为物联网和嵌入式设备设计的管理程序。该项目得益于英特尔代码和工程的贡献，其目标是创建一个灵活小巧的虚拟机管理系统。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 InterruptWindow机制流程图 虚拟机接收到外部中断产生VM_Exi

8、t事件退出到Hypervisor将外部中断转换为虚拟中断并计算虚拟中断优先级当前虚拟机是否开中断？当前最高优先级虚拟中断注入虚拟机返回虚拟机运行状态启动InterruptWindow机制是否一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 InterruptWindow机制流程图 虚拟机执行STI指令是否开启InterruptWindow机制？产生VM_Exit事件退出到Hypervisor重新计算虚拟机虚拟中断优先级注入最高优先级中断到虚拟机返回虚拟机执行状态继续执行是否一个真实的例子-Intel AC

9、RN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 形式化领域模型 InterruptWindowInterruptWindow领域模型六要素：领域模型六要素：虚拟机运行状态虚拟机运行状态 VM_ExitVM_Exit事件处理事件处理 外部中断处理外部中断处理 虚拟中断计算与分发虚拟中断计算与分发 InterruptWindowInterruptWindow计算计算 模型运行起来模型运行起来 一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 构建虚拟

10、机运行状态模型 虚拟机运行状态三要素：虚拟机运行状态三要素：响应外部中断响应外部中断 虚拟中断执行虚拟中断执行 InterruptWindow检测与处理检测与处理 箴言：在箴言：在LTLLTL逻辑里面我们使用一个外部中断集合逻辑里面我们使用一个外部中断集合来表达外部中断在虚拟机运行阶段的响应动作，使来表达外部中断在虚拟机运行阶段的响应动作，使用虚拟中断集合来表达虚拟中断控制器。用虚拟中断集合来表达虚拟中断控制器。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 构建虚拟机运行状态模型 一个真实的例子-In

11、tel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 VM_Exit事件处理 如果如果IRRIRR集合为空表明没有虚拟中断需要注入则集合为空表明没有虚拟中断需要注入则irq_window_enabledirq_window_enabled需要关闭使能，然后跳转需要关闭使能，然后跳转到下一个状态到下一个状态l3l3继续处理继续处理 一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 外部中断处理 ACRNACRN针对外部中断的处理主要是放在针对

12、外部中断的处理主要是放在softirqsoftirq软中断处理软中断处理过程执行，这部分我们只完成一个操作那就是从过程执行，这部分我们只完成一个操作那就是从external_interruptsexternal_interrupts集合里面取出一个中断放入集合里面取出一个中断放入pending_intrpending_intr集合，模拟实际硬件的动作，执行完成后集合，模拟实际硬件的动作，执行完成后跳转到下一个状态跳转到下一个状态l4l4。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 虚拟中断计算与分发

13、 acrnacrn代码设计是放在代码设计是放在acrn_do_intr_processacrn_do_intr_process过程中实现，过程中实现，我们的数学抽象是从我们的数学抽象是从pending_intrpending_intr集合中取出一个中断然集合中取出一个中断然后加入到后加入到vapicvapic集合中，完成虚拟中断的计算与分发注入集合中，完成虚拟中断的计算与分发注入动作，处理完成后继续跳转到下一个状态动作，处理完成后继续跳转到下一个状态l5l5。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验

14、证 InterruptWindow计算 逻辑逻辑模型：模型：执行完毕则跳转到执行完毕则跳转到l1l1即即vm_runvm_run状态模拟状态模拟vm_entryvm_entry指令动作进入虚拟机运行态指令动作进入虚拟机运行态，直接看公式，直接看公式模型可以很容易理解。模型可以很容易理解。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 模型怎样跑起来？心法：心法：InterruptWindowInterruptWindow模型模型是可被多个是可被多个VCPUVCPU线程重入的并发线程重入的并发处理模型，因

15、此需要针对该代码模型进行死锁或异常运行检处理模型，因此需要针对该代码模型进行死锁或异常运行检查，这是确保安全性的关键要素之一，需要我们基于查，这是确保安全性的关键要素之一，需要我们基于该领域该领域模型的推导进一步构造出并发处理模型的数学描述，模型的推导进一步构造出并发处理模型的数学描述，LTLLTL是将是将并发模型表示为时序状态的不确定性组合，因此我们可以使并发模型表示为时序状态的不确定性组合，因此我们可以使用时态逻辑状态机模型来表达这种不确定性组合用时态逻辑状态机模型来表达这种不确定性组合。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN Interr

16、uptWindow软件模型正确性验证 实现：我们可以设计一个时序状态机让这些时序状态并发实现：我们可以设计一个时序状态机让这些时序状态并发运行起来。运行起来。一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型正确性验证 InterruptWindowInterruptWindow模型安全性检查：模型安全性检查：终止性检查终止性检查 正确性检查正确性检查 形式化模型验证 正确性检查：正确性检查：结果正确性结果正确性 过程正确性过程正确性 一个真实的例子-Intel ACRN InterruptWindowIntel A

17、CRN InterruptWindow软件模型正确性验证 结果正确性结果正确性 如果当前如果当前VCPUVCPU除了当前中断还有其他中断要处理并且除了当前中断还有其他中断要处理并且VCPUVCPU处于运行态，那么必须使能处于运行态，那么必须使能InterruptWindowInterruptWindow机机制。制。过程正确性过程正确性 即任意一个即任意一个VCPUVCPU的的pending_intrpending_intr和和vapicvapic集合都为空集合都为空 一个真实的例子-Intel ACRN InterruptWindowIntel ACRN InterruptWindow软件模型

18、正确性验证 深入学习：可以参考我发表的文章 ACRN之InterruptWindow功能正确性形式化验证 怎样用形式化技术推导一个正确模型 理论方法 理论方法 I.I.将原始需求描述进一步抽象使用一阶数理逻辑将原始需求描述进一步抽象使用一阶数理逻辑+集合论建立顶层数集合论建立顶层数理逻辑模型，该模型即是需求的数学规格化描述，是进一步设计理逻辑模型，该模型即是需求的数学规格化描述，是进一步设计求精和验证的依据。求精和验证的依据。II.II.根据顶层数理逻辑模型做设计求精展开成线性时态逻辑表达式，根据顶层数理逻辑模型做设计求精展开成线性时态逻辑表达式，建立时态逻辑规格化描述。建立时态逻辑规格化描述

19、。III.III.如需求涉及到并发体描述则将并发体抽象成时态逻辑加入第二步如需求涉及到并发体描述则将并发体抽象成时态逻辑加入第二步线性时态逻辑规格化描述中。线性时态逻辑规格化描述中。IV.IV.根据需求描述建立时态逻辑属性和数学不变式对线性时态逻辑规根据需求描述建立时态逻辑属性和数学不变式对线性时态逻辑规格化描述进行模型验证。格化描述进行模型验证。物联网操作系统内存管理模型设计推导物联网操作系统内存管理模型设计推导 一个实际案例 物联网操作系统zephyr内存管理模型设计推导 Zephyr内存分配器定义：a.a.内存池定义：内存池是一颗四叉树，树中每个结点代表内存池定义：内存池是一颗四叉树，树

20、中每个结点代表一个物理内存块，每层结点内存块尺寸相同，从树根到一个物理内存块，每层结点内存块尺寸相同，从树根到叶子结点每层内存块尺寸按照从大到小降序排列。叶子结点每层内存块尺寸按照从大到小降序排列。b.b.根据用户指定的内存块大小在内存池中选择一块合适尺根据用户指定的内存块大小在内存池中选择一块合适尺寸的内存块输出。寸的内存块输出。c.c.如果当前内存池没有合适大小的内存块则尝试对当前最如果当前内存池没有合适大小的内存块则尝试对当前最大尺寸内存块进行裂解找到合适内存块输出，如果裂解大尺寸内存块进行裂解找到合适内存块输出，如果裂解失败则报错。失败则报错。d.d.允许多个线程并发访问该功能接口。允

21、许多个线程并发访问该功能接口。顶层逻辑设计顶层逻辑设计 内存池模型设计：内存池模型设计：这里我们选用这里我们选用TLA+TLA+的的Record+FunctionRecord+Function模型来表达这一概念模型来表达这一概念如下：如下：k_mem_poolk_mem_pool为一个为一个recordrecord模型，模型，max_szmax_sz是这颗四叉树顶层最是这颗四叉树顶层最大内存块尺寸，大内存块尺寸，levelslevels是一个是一个functionfunction用来表示树的每一层拥用来表示树的每一层拥有的空闲内存块，每一层空闲块用集合来表达。有的空闲内存块，每一层空闲块用集合

22、来表达。顶层逻辑设计顶层逻辑设计 两个核心概念：两个核心概念：合适尺寸的内存块合适尺寸的内存块 裂解概念裂解概念 顶层逻辑设计顶层逻辑设计 裂解基本原理：裂解基本原理：裂解过程需要一个基于树的层次区间进行，那么我们就必裂解过程需要一个基于树的层次区间进行，那么我们就必须要首先求出需要裂解层次的须要首先求出需要裂解层次的start_levelstart_level和和end_levelend_level，可以，可以分别定义为分别定义为free_levelfree_level、alloc_levelalloc_level，然后我们根据这个区间，然后我们根据这个区间设计一套数学公式来表达这个裂解过程

23、。设计一套数学公式来表达这个裂解过程。顶层逻辑设计顶层逻辑设计 线性时态逻辑模型求精 求精策略：根据顶层逻辑模型的规格化描述，我们将公式里求精策略：根据顶层逻辑模型的规格化描述，我们将公式里面的面的OPERATOROPERATOR进一步展开成状态流用时态逻辑进行表达。进一步展开成状态流用时态逻辑进行表达。技巧性原则：如需求描述涉及到并发体访问则先不考虑并发技巧性原则：如需求描述涉及到并发体访问则先不考虑并发因素，例如我们本例模型可以先考虑非并发模型的求精过程，因素，例如我们本例模型可以先考虑非并发模型的求精过程，之后再逐步加入针对并发体访问逻辑的时序状态描述，实践之后再逐步加入针对并发体访问逻

24、辑的时序状态描述，实践证明这样求精的效率非常高。证明这样求精的效率非常高。线性时态逻辑模型求精 非并发的时态逻辑求精如下：非并发的时态逻辑求精如下：线性时态逻辑模型求精 终止性验证 技术原则：验证过程中如果存在问题在此基础上进行技术原则：验证过程中如果存在问题在此基础上进行调试修改，验证通过后我们再增加针对并发体的时态调试修改，验证通过后我们再增加针对并发体的时态逻辑。逻辑。并发体时态逻辑并发体时态逻辑 并发体时态逻辑并发体时态逻辑 并发体终止性验证并发体终止性验证 正确性验证正确性验证 化简化简:N个线程同时从初始化四叉树模型中申请大小相同的内存块所要满足的预期属性 进一步规格化描述进一步规

25、格化描述 初始化四叉树模型：初始化四叉树模型：N N个线程申请内存块大小：个线程申请内存块大小：预期属性：预期属性：正确性验证正确性验证 出错了？正确性验证正确性验证 原因分析 原因一：四叉树裂解过程中当前层内存块的提取到原因一：四叉树裂解过程中当前层内存块的提取到下一层内存块的裂解之间的操作存在时间空隙可以下一层内存块的裂解之间的操作存在时间空隙可以被其他线程所抢占，这样会导致内存分配不正确导被其他线程所抢占，这样会导致内存分配不正确导致时序状态违例。致时序状态违例。原因二：原因二：L3L3状态分配内存可以被其他线程所抢占造状态分配内存可以被其他线程所抢占造成当前线程内存分配计算的成当前线程

26、内存分配计算的free_lfree_l、alloc_lalloc_l游标与被游标与被抢占后的四叉树模型不一致从而导致内存分配失败抢占后的四叉树模型不一致从而导致内存分配失败产生时序违例。产生时序违例。正确性验证正确性验证 解决方案 针对这两种情况我们考虑将针对这两种情况我们考虑将L3L3、L4L4状态进一步优化状态进一步优化如下：如下：正确性验证正确性验证 再次验证！通过！总结总结 我们的方法虽然只能做到部分形式化，但是基本上工作量已经非常小了，而且项目和设计人员非常容易掌控，最后经过简单的目标测试就可以完成产品目标代码最终的验证工作。需求形式化、设计形式化、验证形式化：软件设计初期往往充满了很多不确定因素，包括对需求概念的理解、原始需求模型的安全性、正确性考虑都不可能做到完全充分清晰的前提下，使用形式化方法从顶层逻辑模型设计阶段就将需求概念模型进行精确描述，那么错误的模型或在求精阶段存在的BUG就可以通过时态逻辑的属性验证发现并进行修改优化。上下一致、验证模型容易向目标代码转换：线性时态逻辑是作为顶层逻辑模型的求精，既保证了与顶层需求模型的一致性同时又保证了求精模型可以在实现层面很容易向目标代码转换。部分形式化大大减少工作量：深入实践深入实践 基于线性时态逻辑的物联网操作系统安全性设计理论。推荐两本书：THANK YOU