（ 序：在发布了软件测试技术应用现状调查报告(一) ，有人就会问：什么是MBT？什么是定理证明？什么是模型检验？ 在发布第二部分调查报告前，先给大家普及一些MBT的知识。征得南京大学卜磊老师同意，这里转发他之前写的、刊登在南京大学计算机系公众号“NJU计小微”的一篇文章，消除大家的疑问。这里直入主题，省略了前面极具幽默风趣的几千字，特别不应该忽视卜老师又酷又帅的照片，如果想看原文和仰慕一下卜老师，点击底部“阅读原文”。 ）
....... 极具幽默风趣的几千字 省去.......
企业采用的测试手段和大家的方法其实类似，说白了就是跑各种用例 尽力覆盖更多的可能，然后去比对运行情况和预期是否一致，或者进一步对代码达到一定的覆盖率。然而，注意到没有，这个过程能不能发现问题和你运行的用例密切相关。虽然相关领域有着大量的研究去自动生成高效的测试用例尽可能覆盖更多的行为，但是对于复杂系统，当它的潜在输入可能非常巨大的时候，你是不是能恰好触发要命的那一个用例这就保不齐了。
举一个所有软工课几乎都会提到的案例，欧洲Ariane5运载火箭因为一行强制转换代码失败，导致火箭上天37秒后变成了一个巨型烟花秀。你要是说他们发射前没好好测试，你信么？反正我是不信的。手机死机了可以重启，LOL出错了你可以换Dota，然而飞机飞在天上的时候怎么重启呢？导弹打出去了怎么收回来更换呢？所以在安全攸关领域，随着程序问题越来越多，后果越来越重，逐渐开始要求在常规测试之外加上一个更严格的检测手段来确保没有问题。这个方法就是形式化证明。
一套公理系统
所谓“形式化”说的简单一点就是将你所要做的事情用严格的无二义性的数学语言描述出来。而“证明”，各位一路数理化读上来的同学都很熟悉。不外乎就是根据已知条件，依据某某公理，可以一步步推导出某某结论。这样的公理系统在计算机领域一样存在，比如大名鼎鼎的霍尔逻辑（Hoare Logic）。霍尔逻辑的核心是霍尔三元组（Hoare Triple），其将一段代码的执行描述成｛P｝C｛Q｝的形式，其中P和Q是原子命题，P称为前置条件，Q称为后置条件，而C是代码命令。这个三元组解读为如果在执行C语句前P成立，则执行C后Q一定成立，比如{P} skip {P}。针对各种代码执行情况，比如赋值，组合，条件判断等，图灵奖获得者Tony Hoare爵士给出了一套公理系统。
而基于这套公理系统，理论上程序员们就可以从你的main函数的第一条初始化命令开始一步一步展开证明，去保证你的代码执行过程中每一步都满足你的预期。比如，你可以为一些关键语句设置一个称之为不变式（invariant）的断言（assertion），然后通过霍尔逻辑去证明执行到这一点时该不变式没有被违反。类似的方法，也就是软件形式化证明的第一个方向——定理证明（Theorem Proving）。这种方法一经提出，便得到了整个计算机行业的重点关注，经过了包括Dijkstra，Hoare，Floyd，Lamport等在内的众多大牛的努力研究，该方法取得了长足的进展，并且在军工,航空等领域得到了切实的应用。而相关公理系统方面的研究，也在从一般简单代码的证明向含有指针、对象等的复杂代码进行挑战。比如我所在软件工程组赵建华教授所提出的Scope Logic就是近期在相关领域的一项突破。Tony Hoare老师本人也对此技术给予了很高的评价。
虽然已经有大量的半自动定理证明工具被开发出来，但是证明这件事情还是需要人来参与其中的。这也就导致了我们很难去指望随便拉个程序员来都可以对一个复杂系统进行严格证明。对于一般用户而言，能通过Push Button的形式点个开始就听着歌等结果是最开心的了。要让他自己去证明？呵呵… 那么证明这件事能不能自动化呢？带着这个问题，科学家们又开始展开了另一个方向的探索。这带来了又一项图灵奖获奖成果——模型检验（Model Checking）。
模型检验的概念是由美国的Edmund Clarke，Allen Emerson和法国的Joseph Sifakis等学者在上世纪80年代分别提出的，他们也因此分享了2007年的图灵奖。话说那年我恰好在Ed Clarke老师组里做访问学生，某天Ed在组会上捧了个金属碗里面塞满了糖给大家分，我们嘻嘻哈哈猜这是有啥喜事了，然后Ed笑嘻嘻指了指装糖的碗，然后大家就愣住了…原来拿了图灵奖是发个碗啊：）
对程序行为空间的自动化遍历
与定理证明强调一步步按照公理系统去展开严格证明推导不同，模型检验依赖的是对程序行为空间的自动化遍历。遍历也就意味着穷尽搜索，所以一开始模型检验技术主要检查的对象是用有穷状态机（Finite State Machine）描述的系统模型。那么检验什么呢？总得有个什么叫对什么叫不对的标准吧。在模型检验领域，一般我们验证的是某个模型是否满足给定的形式化规约（Formal Specification），而关于形式化规约又引出另一项图灵奖成果——时序逻辑（Temporal Logic）（获奖人Amir Pnueli，1996）。所谓时序逻辑说简单点就是将系统行为随着时间应该满足的性质用逻辑公式表达出来。
以线性时序逻辑（Linear Temporal Logic）为例，其引入了包括X（next），G（always），F（eventually），U（until）等时序操作符。比如，对于一个核电站系统，就可以写出这样的规约G（reactor_temperature < A），即在执行过程中,反应器温度永远不能超过A。再举一个例子，在交通灯中我们希望灯在绿色状态时，它将在变为黄色前一直保持绿色，那么我们就可以将其表达成G（green->green U yellow）。
给出一个具体的执行轨迹
好了，现在我们有了系统的模型，有了检验的规约，这两者就 构成了模型检验技术的输入。模型检验技术将自动化的去对系统模型的状态空间进行显式地遍历或者符号化地不动点（fix point）计算来判断该模型的行为是否满足规约的要求，比如会不会出现温度超过A，或者颜色跳错了等。当检查结束时，如果未出现反例，则这个模型对于此规约而言一定是正确的；而如果检查中出现反例，该技术会给出一个具体的执行轨迹，告诉你模型是怎么一步步执行并最终违反了你给出的规约。
由于模型检验技术需要对状态空间做一个穷尽的搜索，所以当系统状态空间过大的时候，该技术的处理能力就会遇到一定问题。说直白一点，如果将这个系统背后可能的状态一个个列出来就能把你电脑内存吃干净甚至于都放不下的话，你还想在上面做搜索，你的计算机一定要哭着臣妾做不到，分分钟死给你看了。
所以，科学家们提出了各种各样的包括符号模型检验（Symbolic Model Checking），偏序约减（Partial Oder Reduction），状态抽象（Abstraction）等在内的一系列优化技术来压缩状态的表达，缩减要验证的空间，提高遍历的效率。随着相关技术的逐步发展，模型检验也终于从实验室走向了应用，在电路设计，协议设计等领域发挥了巨大的作用。比如2009年，Intel的工程师们就在相关领域旗舰会议CAV（Computer Aided Verification）上报告了他们如何成功地将Intel i7处理器的一个核心部件的测试工作全部用模型检验来进行取代。
整体状态空间是一个有穷系统
那么模型检验为什么会首先在硬件领域取得成功呢？答案很简单，因为对于一般的硬件系统，其每个寄存器的取值也就0和1两种可能，这带来的结果就是其整体状态空间是一个有穷系统。那么软件呢？问题一下子又再次复杂起来了。硬件系统如果所有输入我们都可以理解为boolean变量的话，软件则充斥着float，double等变量，定义一个double a，假设有限制0<a<1, 你说a有多少种可能取值？看出来了吧，这是一个无穷状态空间系统。所以想再靠对状态进行遍历来展开验证肯定行不通了。
这个问题 对于其他系统存在吗？事实上，对于一类被称之为实时系统的复杂系统而言，这个问题一样存在。所谓实时系统也就是说这个系统和外界交互时其行为受到时间因素的影响。比如其接受指令后，需要在10毫秒内给出相应；再比如当系统处于某一种工作模式时，其状态变量取值随着时间会发生变化。拿一个简单的烧水壶来说，它有两种工作模式，烧水或者关闭。当其处于烧水模式时，水壶内水温根据dx/dt=0.1x的微分方程上升，当其关闭时，水温根据dx/dt=-0.1x的微分方程下降，水壶会在这两种模式间切换。这时如果检查的规约是系统启动3分钟后水温要控制在20-30度之间，又要如何检查呢？别忘了这时系统中引入了时间t这个变量，不要说3分钟了，0-1秒间有多少时刻，你倒是去遍历呢…
因此如何对上述软件系统、实时系统等无穷状态空间系统进行有效模型检验是当前相关领域主要关注热点所在。如何对状态空间进行符号化表达并求解是其中的一项重要问题。我们软件工程组的老师也在此领域进行了 长期的探索与研究，在实时系统模型检验方面开发的验证工具BACH在国际上引起了广泛关注，得到了来自CMU，UC Berkeley， UBC等多所顶尖院校的科研人员下载试用。
各种新型系统快速涌现
随着整体计算机技术的飞速发展，各种新型系统快速涌现并立刻走向实用。这也是计算机领域的魅力所在。信息物理融合系统（Cyber－Physical System），物联网系统（Internet of Things）等就是近年来的典型代表。相关系统通过传感器、通信、感知等技术在系统运行中获取自身与外界信息，对运行策略进行智能化控制从而可以高效、精准、低耗地完成之前不敢想的各种复杂任务。而这种在开放环境下运行系统的行为又该如何进行验证？这也是近年来相关领域关注的热点所在。那么以后随着新的应用领域突破，新型计算形式出现，又会给系统行为验证，质量保障领域带来什么新的挑战呢？我们一起拭目以待。
