TTT算法

一、背景
(MAT)
这个算法假定了一个“”的角色,他是先知,知道这个黑盒SUL的一切 。在构造过程中我们可以问老师二种类型的问题 。一是称为 query成员查询,对于构造Mealy 来说就是输入某个字串,SUL输出什么?(对于DFA来说,对应于回答这个字串是否被SUL接受,如果接受输出1,否则为0);第二种称为 query(等价查询),即目前构造的DFA或者Mealy自动机和SUL是否等价,如果等价,则回答yes,否则也返回一个反例字串,来说明他们的不同 。如果给出一个反例,需要通过询问额外的问题来完善其假设,从而推测一个后续的新假设 。这些构建假设/改进和等价性检查的步骤被迭代执行,直到等价性查询yes 。
主动自动机学习旨在通过执行测试用例并观察结果(无论输入序列是否合理)
依赖的几个假设
可被调用的操作集合必须是先验已知的(例如,来自公开API)
系统对 query的反应必须是可观察的
系统必须在选定的输出抽象下确定性地运行
【TTT算法】需要一种重置系统的方法,即,后续 query必须是独立的
such , thevery small.
没有作为外部源输入的话,推断的自动机通常很小 。
有监督主动学习的过程中,In case of a , a traceaisto the , which thenits .
当出现一个时,学习算法需要将包含的信息合并到其内部数据结构中 。set,set
举例字符串“”
前缀集为{“A”,“AC”,“ACV”,“ACVS”,“ACVSD”};
后缀集为{“B”,“DB”,“SDB”,“VSDB”,“CVSDB”}
问题描述:可以打开、读取和关闭文件 。只有在以前打开过文件的情况下,才可以阅读和关闭该文件 。文件只有在关闭时才能打开 。此外,还可以写入文件 。这需要将此文件的访问模式设置为预先读/写(chmod rw) 。无法更改打开文件的访问模式 。
难点:chmod rw操作不会立即生效:需要先打开文件,然后写入文件 。因此,由学习算法推断的模型可能是不正确的,如图2b所示 。如果与阅读相比,写入是一种罕见的操作,那么这种不完整性将在很长一段时间内被忽视 。只有当访问模式被设置为读/写并且文件被打开和写入时,假设才不能解释观察到的行为 。图二b不支持下面的序列
前人解决方法:将后缀添加到内部数据结构中;将反例的所有后缀添加到它们的数据结构中;使用反例的所有前缀以确保识别新状态;
局限性:此前的算法会导致所存储的信息用于在随后的细化期间的 query 。多余的打开,读,关闭会一遍遍重复执行,即使不能获得有价值的信息 。此外,由于这些冗余出现在实际兴趣点(chmod rw)之前和之后,因此无论是完全基于前缀的方法还是完全基于后缀的方法都不能避免这个问题 。
目标:消除所有执行反例冗余导致的性能问题 二、方法
假设构建:所选输入符号序列被发送到SUT,观察响应时生成了哪些输出符号序列 。输入序列的选择取决于观察到的对先前序列的响应 。当满足一定的收敛准则时,学习算法构造一个假设,该假设是与迄今为止记录的观测一致的最小确定性Mealy机 。这意味着对于已经发送到SUT的输入序列,该假设产生与从SUT观察到的输出相同的输出 。对于其它输入序列,该假设通过从记录的观测值外推来预测输出 。
假设验证:为了验证这些预测与SUT的行为一致,学习移动到验证阶段,其中SUT经受一致性测试算法,该一致性测试算法旨在验证SUT的行为与假设一致 。如果一致性测试发现了反例,即:如果SUT和假设在输入序列上不一致,则重新进入假设构建阶段,以便构建更精确的假设,该假设也考虑所发现的反例 。如果没有找到反例,学习终止并返回当前假设 。这不是SUT符合假设的绝对保证,尽管许多一致性测试算法在一些技术假设下提供了这样的保证 。如果假设构造和验证的循环没有终止,则这指示SUT的行为不能被有限Mealy机器捕获,该有限Mealy机器的大小和复杂性在所采用的学习算法的范围内 。