从歧义到显式：用于形式化分析的 NLP 辅助 5G 规范抽象
计算与语言
2023-08-08 v1
摘要
基于形式化方法的 5G 无线通信协议分析对于识别逻辑漏洞并促进全面安全评估至关重要，尤其在设计与规划阶段。自然语言处理（NLP）辅助技术和大多数工具尚未被工业界与研究领域广泛采用。传统的通过数学方法的形式化验证严重依赖手动逻辑抽象，易耗时且易出错。NLP 辅助方法未应用于工业研究的原因可能在于协议设计的自然语言存在歧义性，这与形式化验证的显式性相矛盾。为应对在协议设计中采用形式化方法的挑战，针对以自然语言编写的（3GPP）协议，本研究提出一种混合方法来简化协议分析。我们引入一个两步流水线，首先使用 NLP 工具构建数据，然后利用所构建数据通过 NLP 模型提取标识符与形式化属性。标识符与形式化属性进一步用于形式化分析。我们实现了三个模型，以标识符与形式化属性之间的不同依赖关系为准则。最优模型的结果在标识符提取上达到 39% 的有效准确率，在形式化属性预测上达到 42%。我们的工作为大规模复杂规范与协议（尤其是 5G 及下一代通信）形式化分析的高效流程提供了概念验证。
引用
@article{arxiv.2308.03277,
title = {From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis},
author = {Shiyu Yuan and Jingda Yang and Sudhanshu Arya and Carlo Lipizzi and Ying Wang},
journal= {arXiv preprint arXiv:2308.03277},
year = {2023}
}