形式化验证的原理和过程

形式化验证包含两种方式：定理证明（数学定理的方式，所以对任意状态数的系统都适用，缺点是不能很好的给出反例），模型检测（主要是进行所有的状态检测，并能给出反例，缺点是存在复杂系统的状态爆炸问题）。模型检测我没有研究，这里不谈，但是分别都有大量学术研究，也能搜到大量博客文章。

所以下面指的形式化验证就是定理证明这个方式。定理证明中，coq工具用的人很多，所以下面指的就说coq验证过程，其实，别的证明工具的证明过程也是类似的。

本质

形式化验证就是通过数学方法对程序有一个精细的，准确的描述和认识。所以定理证明是白盒测试，而用例测试属于黑盒测试，因为它不需要知道被验证对象的内部结构。

形式化证明coq代码的编写，不应该是当作编程的思维来对待，而是初高中做数学证明题一样的思维，因为它就是一个辅助的代替笔和纸来手写的工具，可以方便的引用一些已经证明过的引理进来，能用simplify等关键字来做一些显而易见的自动化的化简而已，核心证明思路都得自己去引导的。除了显而易见的步骤，你别期望它能做更多，因为他不会比你聪明，你都不知道怎么往下证明的，它也不会知道的。但是也说不定，多年以后，真正的定理自动证明工具成熟了，说不定就越来越聪明，能自动帮我们证明出我们都不会证明的定理。

因为coq只是提供一个证明工具环境，所有的基础定理都得我们自己去构建和证明的，比如0+1=1。但是如果对于复杂系统的验证，这样我们就得写很多的验证代码，因此，可能很多公共的引理，不用我们自己去证了，github已经有人都证明好了，整理成了库，我们直接导入，然后引用这些引理就行了。此外，很多数据结构类型，比如集合什么的，coq官方也都给我们定义好了，我们直接导入使用即可，不然我们也得自己去构建和定义的。

用途

形式化验证可以对任何具有逻辑流程的对象进行验证，包括程序代码，法律条文，协议规定等。但是主要对程序代码验证用得较多。

流程

形式化验证的流程：

对被验证对象建立准确的模型
然后对它提出我们期待的性质
然后对这些性质进行证明。

这里就以C语言程序验证为例，来说明问题。现在需要一个用于数列从小到大排序的C语言程序。

这里面会涉及到3个人，分别为A、B、C。

A：提出一个程序设计需求：将一列数从小到大排序

B：负责实现这个算法代码，或许是通过冒泡排序，也可能是快排算法，或者是其它的。

C：负责对B写的这个程序进行形式化验证，看看是否满足A提出的性质。这里的性质，是需求的具体化（一定是具体的，可证明的，为满足需求服务的），仍然是A来提这些性质的（因为他提的需求，当然知道这个程序得满足哪些性质）。比如

性质1 ：当数列为1个数时，总是原样输出。
性质2：当数列多于一个数时，对于任意的非最右端的数，总是小于右边的数的。
性质3：xxx

如果C验证（就是对这些性质进行证明，看看能否通过）后发现，B写的这个程序，都满足了A说的这些性质，那么我们就说B这个程序对于这些指定的性质完全正确了。我们会发现，形式化验证不是穷举的方式，而是数学推导证明的方式，所以才能下结论：对于指定的性质方面，这个程序的实现完全正确了。但是软件用例测试，就不能下这个结论，除非把所有的情况都给穷举出来测试了。但是这些之外的性质方面，程序是否也是对的呢，这个就不一定了，比如性质没有提到数组越界这方面，那么程序还是有可能会发生越界情况的。所以性质的完备性，是不存在的，这个就是靠有经验的人提的性质，那么会越全面，准确，实际。

说明

形式化验证过程的第一步，对这个被验证程序代码进行建模。建立的模型主要包括两部分，一个是数据结构建立模型，另一个是函数执行过程进行建模。 coq学习3-形式化证明的直观理解_我是标同学的博客-CSDN博客_形式化证明

而建模的准确性（建的模型是否符合被验证对象）也是需要进行形式化验证的，这个就有点像递归套娃了，所以是个无解的问题，解决方法有3个：

通过简单的用例测试来测试我们建立的模型，和被验证对象是否有一样的表现，这个做法简单，但是严谨性不高。
比较严谨的做法是，用一个经过验证的工具对被验证对象自动化生成模型（这个模型往往难以直观读懂），然后与我们的模型进行人工对比，来确认我们建模的准确性，该方法就是自动生成的模型很难读懂，所以对比起来难度有点大。
另一个比较严谨的做法则相反，用一个经过验证的工具对我们建立的模型自动生成被验证对象（容易读懂），然后与我们要验证的实际对象进行人工对比，来确认我们建模的准确性。这个方法比较常用。这种方式还能直接在coq里面建模，验证通过后，直接生成C语言代码，这样一个程序就得到了，这种方式产生的C语言代码天然的可靠的，有些团队也这样开发过程。

建立了模型后，我们就对性质进行证明，看看是否能通过即可。

形式化验证，需要写的验证代码是非常多的，我们原本被验证的C语言程序的代码行数和coq代码行数比例是1：20，所以形式化验证的代价非常大。因此形式化验证一般用于系统中一些安全关键模块的验证，比如飞机控制器的代码等。

可以参考的比较好的学习形式化验证coq博客：

coq学习笔记_我是标同学的博客-CSDN博客_coq语言

coq形式化验证学习进阶_我是标同学的博客-CSDN博客

《软件基础》- COQ 函数式编程 - 知乎入门一下

Coq 入门级技巧 - 知乎 评论说是最好的入门文章

迈克·纳哈斯的Coq教程（中文翻译） - chesium - 博客园讲得比较原理性的博客，值得看看

Software Foundations coq的官方教程，分为6本书，第一本是入门，可以看看。可以看到，所有内容其实还是很多的。

知乎上还有大量的文章写这个coq入门，大家可以去看看。

coq编程好用的编码工具：

coq程序编写好用的IDE推荐_我是标同学的博客-CSDN博客

形式化验证的原理和过程相关推荐

linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
国产自主可控的形式化验证代码自动生成工具ModelCoder可替代Matlab/Sumlink
在安全关键领域,基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具对算法或者控制逻辑进行可视化建模,然后生成高可靠的二进制代码逐渐成 ...
两个简单的Demo示例向读者展示Flash和ASP.NET交互原理以及过程
ASP.NET与FLASH交互学习了ASP.NET的基础知识之后,终于等到学习交互的时候了.请大家和我一起来进行让人激动的交互吧!本章我将用两个简单的Demo示例向读者展示Flash和ASP.NET交 ...
计算机指纹识别的原理步骤,指纹识别原理和过程
指纹识别概念指纹识别是生物识别的一种.不过其所分析的对象是指纹特征.指纹特征是最早被发现和应用的,所以指纹识别的历史较之其它识别技术要悠久的多.出现自动化的指纹识别系统到现在,目前的指纹识别技术已经 ...
基于Token的身份验证的原理
目录 1 发展史 2 Cookie 3 Session 3.1 cookie和session的区别 4 Token 4.1 传统方式--基于服务器的验证 4.2 基于服务器验证方式暴露的一些问题 4. ...
【微信小程序控制硬件④】深度剖析微信公众号配网 Airkiss 原理与过程，esp8266如何自定义回调参数给微信，实现绑定设备第一步！（附带源码）
[微信小程序控制硬件第1篇 ] 全网首发,借助 emq 消息服务器带你如何搭建微信小程序的mqtt服务器,轻松控制智能硬件! [微信小程序控制硬件第2篇 ] 开始微信小程序之旅,导入小程序Mqtt客户 ...
电口以太网物理层一致性测试原理与过程
电口以太网物理层一致性测试原理与过程关键字: 以太网物理层一致性测试 1. 以太网物理层信号特点以太网对应OSI七层模型的数据链路层和物理层,对应数据链路层的部分又分为逻辑链路控制子 ...
linux内核形式化验证,说说形式化验证（Formal Verification）吧
原标题:说说形式化验证(Formal Verification)吧前言:被@暴走恭亲王点名,不得不写这个小文,笔者学识浅薄,而形式化验证这个题目不但大,而且深,笔者掌握的数学知识在专业人士里也就是幼 ...

形式化验证的原理和过程

本质

用途

流程

说明

形式化验证的原理和过程相关推荐

最新文章

热门文章