Annotating Control-Flow Graphs for Formalized Test Coverage Criteria

• URL: http://arxiv.org/abs/2407.04144v1
• Date: Thu, 4 Jul 2024 20:13:03 GMT
• Title: Annotating Control-Flow Graphs for Formalized Test Coverage Criteria
• Authors: Sean Kauffman, Carlos Moreno, Sebastian Fischmeister,
• Abstract summary: We show how to annotate a Control-Flow Graph with decision information inferred from the graph itself. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.
• Score: 0.3277163122167433
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible. Despite their importance, these coverage criteria are often misunderstood. One problem is that their definitions are typically written in natural language specification documents, making them imprecise. Other works have proposed formal definitions using binary predicate logic, but these definitions are difficult to apply to the analysis of real programs. Control-Flow Graphs (CFGs) are the most common model for analyzing program logic in compilers, and seem to be a good fit for defining and analyzing coverage criteria. However, CFGs discard the explicit concept of a decision, making their use for this task seem impossible. In this paper, we show how to annotate a CFG with decision information inferred from the graph itself. We call this annotated model a Control-Flow Decision Graph (CFDG) and we use it to formally define several common coverage criteria. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.

Related papers

• CoGS: Model Agnostic Causality Constrained Counterfactual Explanations using goal-directed ASP [1.5749416770494706]
  CoGS is a model-agnostic framework capable of generating counterfactual explanations for classification models. CoGS offers interpretable and actionable explanations of the changes required to achieve the desired outcome.
  arXiv  Detail & Related papers  (2024-10-30T00:43:01Z)
• Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
  We propose an automated methodology based on metamodeling techniques which consist of two main steps. First, an untimed algorithmic description written in C++ is verified in an early stage using generated assertions. Second, this algorithmic description is verified against its sequential design using HLEC and the respective metamodel parameters.
  arXiv  Detail & Related papers  (2024-10-24T06:09:40Z)
• Automatically Adaptive Conformal Risk Control [49.95190019041905]
  We propose a methodology for achieving approximate conditional control of statistical risks by adapting to the difficulty of test samples. Our framework goes beyond traditional conditional risk control based on user-provided conditioning events to the algorithmic, data-driven determination of appropriate function classes for conditioning.
  arXiv  Detail & Related papers  (2024-06-25T08:29:32Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Scalable Defect Detection via Traversal on Code Graph [10.860910384163892]
  We introduce QVoG, a graph-based static analysis platform for detecting defects and vulnerabilities. It employs a compressed CPG representation to maintain a reasonable graph size, thereby enhancing the overall query efficiency. For projects consisting of 1,000,000+ lines of code, QVoG can complete analysis in approximately 15 minutes, as opposed to 19 minutes with CodeQL.
  arXiv  Detail & Related papers  (2024-06-12T11:24:52Z)
• ProTeCt: Prompt Tuning for Taxonomic Open Set Classification [59.59442518849203]
  Few-shot adaptation methods do not fare well in the taxonomic open set (TOS) setting. We propose a prompt tuning technique that calibrates the hierarchical consistency of model predictions. A new Prompt Tuning for Hierarchical Consistency (ProTeCt) technique is then proposed to calibrate classification across label set granularities.
  arXiv  Detail & Related papers  (2023-06-04T02:55:25Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• 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)
• Pass-Fail Criteria for Scenario-Based Testing of Automated Driving Systems [0.0]
  This paper sets out a framework for assessing an automated driving system's behavioural safety in normal operation. Risk-based rules cannot give a pass/fail decision from a single test case. This considers statistical performance across many individual tests.
  arXiv  Detail & Related papers  (2020-05-19T13:13:08Z)
• Structured Prediction with Partial Labelling through the Infimum Loss [85.4940853372503]
  The goal of weak supervision is to enable models to learn using only forms of labelling which are cheaper to collect. This is a type of incomplete annotation where, for each datapoint, supervision is cast as a set of labels containing the real one. This paper provides a unified framework based on structured prediction and on the concept of infimum loss to deal with partial labelling.
  arXiv  Detail & Related papers  (2020-03-02T13:59:41Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

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.