Diagnosing Violations of State-based Specifications in iCFTL

• URL: http://arxiv.org/abs/2509.17776v1
• Date: Mon, 22 Sep 2025 13:40:02 GMT
• Title: Diagnosing Violations of State-based Specifications in iCFTL
• Authors: Cristina Stratan, Claudio Mandrioli, Domenico Bianculli,
• Abstract summary: We propose a diagnostic approach based on backward data-flow analysis to determine the relevant statements contributing to a specification violation.<n>We implement our approach in a prototype tool, iCFTL-Diagnostics, and evaluate it on 112 specifications across 10 software projects.<n>Our tool achieves 90% precision in identifying relevant statements for 100 of the 112 specifications.
• Score: 1.1059590443280727
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As modern software systems grow in complexity and operate in dynamic environments, the need for runtime analysis techniques becomes a more critical part of the verification and validation process. Runtime verification monitors the runtime system behaviour by checking whether an execution trace - a sequence of recorded events - satisfies a given specification, yielding a Boolean or quantitative verdict. However, when a specification is violated, such a verdict is often insufficient to understand why the violation happened. To fill this gap, diagnostics approaches aim to produce more informative verdicts. In this paper, we address the problem of generating informative verdicts for violated Inter-procedural Control-Flow Temporal Logic (iCFTL) specifications that express constraints over program variable values. We propose a diagnostic approach based on backward data-flow analysis to statically determine the relevant statements contributing to the specification violation. Using this analysis, we instrument the program to produce enriched execution traces. Using the enriched execution traces, we perform the runtime analysis and identify the statements whose execution led to the specification violation. We implemented our approach in a prototype tool, iCFTL-Diagnostics, and evaluated it on 112 specifications across 10 software projects. Our tool achieves 90% precision in identifying relevant statements for 100 of the 112 specifications. It reduces the number of lines that have to be inspected for diagnosing a violation by at least 90%. In terms of computational cost, iCFTL-Diagnostics generates a diagnosis within 7 min, and requires no more than 25 MB of memory. The instrumentation required to support diagnostics incurs an execution time overhead of less than 30% and a memory overhead below 20%.

Related papers

• InspectCoder: Dynamic Analysis-Enabled Self Repair through interactive LLM-Debugger Collaboration [71.18377595277018]
  Large Language Models (LLMs) frequently generate buggy code with complex logic errors that are challenging to diagnose.<n>We present InspectCoder, the first agentic program repair system that empowers LLMs to actively conduct dynamic analysis via interactive debugger control.
  arXiv  Detail & Related papers  (2025-10-21T06:26:29Z)
• Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended) [49.46686813437884]
  We show that it is possible to compute data-aware optimal alignments in a rich setting with general data types and data conditions.<n>This is achieved by carefully combining the two best-known approaches to deal with control flow and data dependencies.
  arXiv  Detail & Related papers  (2025-06-30T10:16:21Z)
• Computation Tree Logic Guided Program Repair [10.880298593486671]
  This paper suggests a mechanism for the automated repair of infinite-state programs guided by CTL properties.<n>Our framework encodes the program and CTL properties into Datalog facts and rules and performs the repair by modifying the facts to pass the analysis rules.<n>Our approach achieves analysis accuracy of 56.6% on a small-scale benchmark and 88.5% on a real-world benchmark, outperforming the best baseline performances of 27.7% and 76.9%.
  arXiv  Detail & Related papers  (2025-02-21T09:59:38Z)
• Search-based Trace Diagnostic [7.771496745635823]
  When an execution trace violates a requirement, engineers need to understand the cause of the breach. This paper proposes search-based trace-diagnostic (SBTD), a novel trace-diagnostic technique for CPS requirements.
  arXiv  Detail & Related papers  (2024-06-25T04:24:21Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. Checking these process constraints is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. We present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change.
  arXiv  Detail & Related papers  (2023-12-20T13:26:31Z)
• FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
  FastDiag is a typical direct diagnosis algorithm that supports diagnosis calculation without predetermining conflicts. We propose a novel algorithm, so-called FastDiagP, which is based on the idea of speculative programming. This mechanism helps to provide consistency checks with fast answers and boosts the algorithm's runtime performance.
  arXiv  Detail & Related papers  (2023-05-11T16:26:23Z)
• Measuring Rule-based LTLf Process Specifications: A Probabilistic Data-driven Approach [2.5407767658470726]
  Declarative process specifications define the behavior of processes by means of rules based on Linear Temporal Logic on Finite Traces. In a mining context, these specifications are inferred from, and checked on, multi-sets of runs recorded by information systems. We propose a technique that measures the degree of satisfaction of specifications over event logs.
  arXiv  Detail & Related papers  (2023-05-09T13:07:01Z)
• PULL: Reactive Log Anomaly Detection Based On Iterative PU Learning [58.85063149619348]
  We propose PULL, an iterative log analysis method for reactive anomaly detection based on estimated failure time windows. Our evaluation shows that PULL consistently outperforms ten benchmark baselines across three different datasets.
  arXiv  Detail & Related papers  (2023-01-25T16:34:43Z)
• Execution Time Program Verification With Tight Bounds [6.36836017515443]
  This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs.
  arXiv  Detail & Related papers  (2022-10-20T09:02:13Z)
• Anytime Diagnosis for Reconfiguration [52.77024349608834]
  We introduce and analyze FlexDiag which is an anytime direct diagnosis approach. We evaluate the algorithm with regard to performance and diagnosis quality using a configuration benchmark from the domain of feature models and an industrial configuration knowledge base from the automotive domain.
  arXiv  Detail & Related papers  (2021-02-19T11:45:52Z)
• An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
  We introduce a divide-and-conquer based diagnosis algorithm (FastDiag) which identifies minimal sets of faulty constraints in an over-constrained problem. We compare FastDiag with the conflict-directed calculation of hitting sets and present an in-depth performance analysis.
  arXiv  Detail & Related papers  (2021-02-17T19:55:42Z)
• Feature Engineering for Scalable Application-Level Post-Silicon Debugging [0.456877715768796]
  We present solutions for both observability enhancement and root-cause diagnosis of post-silicon System-on-Chips (SoCs) validation. We model specification of interacting flows in typical applications for message selection. We define diagnosis problem as identifying buggy traces as outliers and bug-free traces as inliers/normal behaviors.
  arXiv  Detail & Related papers  (2021-02-08T22:11:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.