自动从行为样本中挖掘LTL规范，解决形式化验证的规格难题
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
- 基于系统正负例行为，自动生成LTL逻辑公式作为规范
- 涵盖约束求解、神经网络、枚举搜索等多种技术路径
- 适合形式化方法研究者和需要自动化验证的工程实践者
几乎所有基于形式化方法的验证技术都依赖于精确的正式规格说明，但手动编写规格仍是一项艰巨且易出错的任务。为突破这一瓶颈，近期研究聚焦于从（理想与非理想）系统行为示例中自动生成用于形式化验证的规格说明。本综述系统梳理并比较了近年来在时序逻辑（LTL）领域挖掘规格的进展。多种方法被提出以应对不同设计场景与设置，所用技术涵盖约束求解、神经网络训练、枚举搜索等。本文总结当前最先进技术，并为形式化方法从业者提供对比参考。
原文摘要 · Abstract (English)
Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously challenging and error-prone. To address this bottleneck in formal verification, recent research has thus focussed on automatically generating specifications for formal verification from examples of (desired and undesired) system behavior. In this survey, we list and compare recent advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning LTL formulas, which address different aspects and settings of specification design. Moreover, the approaches rely on a diverse range of techniques such as constraint solving, neural network training, enumerative search, etc. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。