华东师范大学学报(自然科学版)

作者：张枨宇, 诸嘉逸, 黄怿豪, 杨迪, 李建文, 缪炜恺, 阎迪, 顾斌, 詹乃军, 蒲戈光

单位：张枨宇, 男, 博士后, 研究方向为软件工程、形式化方法. >

关键词：模型检查,与非图,组合模型检查器,

与非图模型是一种表示电路设计的通用基础形式, 同时也是模型检查器的一种通用输入格式. 介绍了一种基于与非图结构编码的特征提取方法, 并基于该方法实现了一种快速的组合模型检查器Liquid. 所提出的结构编码的核心思想: 首先罗列出与非图中所有可能的子结构, 再将每个子结构出现的次数编码成向量, 该向量即作为与非图的特征向量参与之后的机器学习过程. 由于各种模型检查算法的性能在不同的与非图上参差不齐, Liquid的设计目标是组合多种模型检查算法, 针对不同的与非图使用机器学习模型挑选出合适的算法. 收集了目前所有的模型检查器基准测试集作为实验数据集并进行了实验. 实验结果表明, Liquid在实验数据集上的表现优于所有组合中的独立模型检查算法, 并有着不错的预测准确率. 同时, 还从多个维度分析了Liquid有效的原因.

来源：2024年第4期

《华东师范大学学报(自然科学版)》期刊编辑部

查看华东师范大学学报(自然科学版)杂志2024年第4期