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
- 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]
Dafny and F* provide means to formally specify and prove properties of programs.
There is no algorithmic way of ensuring the correctness of the user-intent formalization for programs.
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) - Stateless and Rule-Based Verification For Compliance Checking
Applications [1.7403133838762452]
We present a formal logic-based framework for creating intelligent compliance checking systems.
SARV is a verification framework designed to simplify the overall process of verification for stateless and rule-based verification problems.
Based on 300 data experiments, the SARV-based compliance solution outperforms machine learning methods on a 3125-records software quality dataset.
arXiv Detail & Related papers (2022-04-14T17:31:33Z) - Prioritized Variable-length Test Cases Generation for Finite State
Machines [0.09786690381850353]
Model-based Testing (MBT) is an effective approach for testing when parts of a system-under-test have the characteristics of a finite state machine (FSM)
This paper presents a test generation strategy that satisfies all these requirements.
Depending on the application of the FSM, the strategy and evaluation presented in this paper are applicable both in testing functional and non-functional software requirements.
arXiv Detail & Related papers (2022-03-17T20:16:45Z) - 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.