一句话：提出 PURLTL，用神经搜索与正例-未标注学习从不完美轨迹挖掘任意 LTL 规约，大幅超越 SOTA。
形式化规约广泛用于软件测试，但人工编写费时。现有从轨迹挖掘 LTL 规约的方法存在不足：忽视不完美轨迹（部分剖析、上下文缺失或有缺陷程序）、依赖模板导致表达力受限、需要实际中难以获得的负轨迹。本文提出 PURLTL，从不完美轨迹挖掘任意 LTL 规约。为缓解搜索空间爆炸与错误偏置，它用神经网络搜索 LTL 公式，通过可微分参数操作模拟 LTL 路径检查；针对缺少负轨迹，将问题转化为正例-未标注学习，并结合数据增强进行 PU 学习。实验表明其大幅超越先前 SOTA，且对不完美轨迹鲁棒、不依赖公式模板。
Formal specifications are widely used in software testing approaches, while writing such specifications is a time-consuming job. Recently, a number of methods have been proposed to mine specifications from execution traces, typically in the form of linear temporal logic (LTL). However, existing works have the following disadvantages: (1) ignoring the negative impact of imperfect traces, which come from partial profiling, missing context information, or buggy programs; (2) relying on templates, resulting in limited expressiveness; (3) requesting negative traces, which are usually unavailable in practice. In this paper, we propose PURLTL, which is able to mine arbitrary LTL specifications from imperfect traces. To alleviate the search space explosion and the wrong search bias, we propose a neural-based method to search LTL formulae, which, intuitively, simulates LTL path checking through differentiable parameter operations. To solve the problem of lacking negative traces, we transform the problem into learning from positive and unlabeled samples, by means of data augmentation and applying positive and unlabeled learning to the training process. Experiments show that our approach surpasses the previous start-of-the-art (SOTA) approach by a large margin. Besides, the results suggest that our approach is not only robust with imperfect traces, but also does not rely on formula templates.
@inproceedings{PengLHLDWYZ23,
title = {PURLTL: Mining LTL Specification from Imperfect Traces in Testing},
author = {Bo Peng and Pingjia Liang and Tingchen Han and Weilin Luo and Jianfeng Du and Hai Wan and Rongzhen Ye and Yuhang Zheng},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00202}
}