正文
图.4
Peled 等人和 Steffen 等人的开创性工作在模型学习和正式方法的领域之间建立了迷人的联系，特别是模型检验和基于模型的测试。随后的研究已经证实，在没有反应系统的易处理的白箱模型的情况下，学习模型通常是可以以相对低的成本获得的优良的替代方案。
为了检查学习模型的属性，可以使用模型检查（model checking）。事实上，Peled 等人已经在一种叫「黑箱检查（black box checking）」的方法中展示了如何完全整合模型学习与模型检查，其基本思想是使用模型检查器作为图 4 中一致性测试工具的「预处理器（preprocessor）」。当教师接收到学习器的假设时，首先运行模型检查器以验证假设模型是否满足 SUL 规定的所有属性。只有假设为真时，才转发给一致性测试器（conformance tester）。如果其中一个 SUL 属性不成立，那么模型检查器产生一个反例。现在有两种情况。第一种可能性是反例可以在 SUL 上再现。这意味着我们已经在 SUL（或其规定中）中展示了一个错误，我们停止学习。第二种可能性是反例不能在 SUL 上再现。在这种情况下，教师遵循假设是不正确的原则向学习器返回反例。在后来的工作中，黑箱检查方法已经进一步完善，并已成功应用于几个工业案例。
大多数学习算法的所需会员查询数量随着输入数量线性增长，并与状态数量成二次方。这意味着当输入数量增长时，学习算法规模相当好；换句话说，制定一个新的假设是容易的。然而，检查假设是否正确（一致性测试）会很快成为大量输入的瓶颈。如果当前假设具有 n 个状态，则 SUL 具有 n' 个状态，并且存在 k 个输入，则在最坏的情况下，需要运行包含 n'-n 个输入的所有可能序列的测试序列，即 k(n' − n) 个可能性。因此，模型学习目前只能应用于少于 100 个输入的情况下。因此，我们寻求帮助我们减少输入数量的方法。
抽象（abstraction）是将模型学习方法扩展到现实应用程序的关键。Cho 等人通过在僵尸网络服务器和学习软件之间放置仿真器/映射器（emulator/mapper），将字母符号具体化为有效的网络消息并将它们发送到僵尸网络服务器（botnet servers），成功推断出现实僵尸网络命令和控制协议的模型。当接收到响应时，仿真器作反向处理：它将响应消息抽象为输出的字母，并将它们传递到学习软件。这种学习设置的示意图概述如图 5 所示。处理抽象的中间映射器组件的想法是非常自然的，并且在许多关于自动机学习的案例研究中被隐含地或明确地使用。Aarts 等人通过与谓词抽象（predicate abstraction）和抽象解释（abstract interpretation）建立连接，发展出了关于中间性抽象（intermediate abstraction）的数学理论。
图.5
一个补充性的简单但实用的方法是将模型学习应用在多个更小的输入子集上。这将明显降低学习复杂性；还因为对于有限数量的刺激，可达状态的集合通常将更小。然后，对于输入的子集学习的模型可以用于在学习更大子集的模型时生成反例。例如，Chalupar 等人已经应用的另一种方法是将通常以特定顺序发生的多个输入动作合并成单个高级动作，从而减少输入的数量。再次，已经用少量高级输入学习的模型可以用于在后续实验中产生反例，其中这些输入被分解成它们的组成部分。
正如 C.A.R. Hoare 所说，一个人可以说，在每个大程序中都有一个小的状态机试图出去。通过选择适当的输入动作集合并定义适当的映射器/抽象，我们可以使这个小状态机对学习者可见。
应用案例
近年来，模型学习已经成功应用于不同领域的许多实际案例。工业应用的例子有，例如，在西门子的电信系统的回归测试（regression testing），在法国电信的集成测试，在施普林格出版社线上会议的自动测试，在沃尔沃科技的线控制动系统的测试要求。下面，我将概述奈梅亨大学（Radboud University）在智能卡、网络协议和遗产软件（legacy software）方面进行的一些代表性案例研究。
智能卡。
Chalupar 等人使用模型学习来反向工程 e.dentifier2——一种用于网上银行的智能卡阅读器。为了能够学习 e.dentifier2 的模型，作者构建了一个由树莓派（Raspberry Pi）控制的乐高机器人，可以操作读取器的键盘（参见图 6）。从笔记本电脑控制所有这些之后，他们可以使用 LearnLib 学习 e.dentifier2 的模型。他们学习了一个版本的 e.dentifier2 的四态 Mealy 机，揭示了存在的一个安全缺陷，并且表明该缺陷不再存在于新版本设备的三态模型中。
图.6
在另一项研究中，Aarts 等人学习了银行卡上的 EMV 协议套件的实现模型，这些银行卡有来自几家荷兰和德国银行的，有荷兰和瑞典银行发行的万事达信用卡以及一张英国签证借记卡。为了学习模型，LearnLib 对每个卡执行 855 到 1696 个会员和测试查询，并生成 4 到 8 个状态的模型。（图 7 展示了其中一个学习的模型）。所有卡产生不同的模型，只有荷兰银行卡上的应用程序是相同的。所学到的模型没有揭示任何安全问题，虽然注意到一些怪异问题。作者认为，模型学习将作为安全评估的一部分发挥作用。
图.7
网络协议。
我们的社会已完全依赖于网络和安全协议的正确运作；这些协议中的错误或漏洞可能会导致安全漏洞甚至是彻底的网络故障。模型检查已被证明是一种用于发现此类错误与漏洞的有效技术。然而，由于针对协议实现的详尽模型检查通常不可行，因此模型检查通常会应用于根据协议标准开始人工制作的模型。这意味着由于协议实现不符合模型检查的规范，其出现的错误便无法被捕捉。研究证明，模型学习能够有效地找到此类错误，使这项技术得以与模型检查互补。
例如，De Ruiter 和 Poll 使用支持多种密钥交换算法和客户端认证选项的测试工具分析了 TLS 协议的服务器端和客户端实现。结果表明模型学习（或称为协议状态模糊）可以捕获一类有趣的实现缺陷，而这种缺陷在安全协议实现中十分常见：在九个受测试的 TLS 实现中，有三个能够发现新的安全缺陷。如 Java Secure Socket Extension 便是一类学习了 Java 1.8.0.25 版本的模型。他们发现该模型包含两条通往应用程序数据交换的路径：常规 TLS 协议运行和另一意外运行。客户端以及服务器应用程序都以为它们处于安全的连接上交谈，但实际上任何人都能够通过利用这种行为读取并篡改客户端的数据。所以修复作为安全更新的一个关键部分而被发布，并且他们能够通过学习 JSSE 1.8.0.31 版本的模型来确认问题是否已解决。得益于人工构建的抽象/映射器，经验丰富的 Mealy 机包含 6 至 16 个状态并且规模都很小。另外，由于对不同的 TLS 实现的分析产生了独一无二的 Mealy 机，模型学习也可用于为 TLS 实现添加指纹印记。
Fiterau 等人在一个涉及 Linux、Windows 以及使用 TCP 服务器与客户端的 FreeBSD 实现的案例研究中将模型学习与模型检查进行了结合。模型学习用于推断不同组件的模型，而后应用模型检查来充分探索当这些组件（如 Linux 客户端和 Windows 服务器）交互时可能的情况。案例研究揭示了 TCP 实现中不符合其 RFC 规范的几个例子，具体示例参见图 8。
