Scholarlink

<p>With the increasing complexity and interconnection of systems, along with growing demands for high reliability and security, the verification of program correctness over finite execution traces has received increasing attention. However, existing symbolic execution and software model checking methods exhibit significant limitations in expressing and verifying temporal properties over finite traces, particularly in effectively capturing and checking complex temporal relationships between events within programs. To address this issue, this paper proposes a model checking approach guided by linear temporal logic over finite traces (LTLf). This approach embeds LTLf properties into program execution, transforming temporal property verification into assertion checking, thereby enabling effective monitoring and detection of temporal behaviors over finite traces. Based on this method, we implemented the <InlineEquation ID="IEq3"> <EquationSource Format="TEX">\(\textbf{CPD}_{\textbf{LTLf}}\)</EquationSource> </InlineEquation> tool and validated its effectiveness through experiments on two programs. The results demonstrate that the approach can accurately identify potential paths violating LTLf properties, showing promising practicality and detection precision.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

CPD\(_{\textrm{LTLf}}\) : a linear temporal logic over finite traces guided model checking tool

  • 期刊论文

  • 发表日期：

    2025年9月29日

查看全文
  • Xiangqi Zeng,
  • Meng Wang,
  • Miao Wang,
  • Xu Lu

摘要

With the increasing complexity and interconnection of systems, along with growing demands for high reliability and security, the verification of program correctness over finite execution traces has received increasing attention. However, existing symbolic execution and software model checking methods exhibit significant limitations in expressing and verifying temporal properties over finite traces, particularly in effectively capturing and checking complex temporal relationships between events within programs. To address this issue, this paper proposes a model checking approach guided by linear temporal logic over finite traces (LTLf). This approach embeds LTLf properties into program execution, transforming temporal property verification into assertion checking, thereby enabling effective monitoring and detection of temporal behaviors over finite traces. Based on this method, we implemented the \(\textbf{CPD}_{\textbf{LTLf}}\) tool and validated its effectiveness through experiments on two programs. The results demonstrate that the approach can accurately identify potential paths violating LTLf properties, showing promising practicality and detection precision.