2018年领域模型与形式化验证技术.pdf

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