Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

• URL: http://arxiv.org/abs/2401.14320v1
• Date: Thu, 25 Jan 2024 17:18:33 GMT
• Title: Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
• Authors: Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber, Robert Heinrich, Alexander Weigl
• Abstract summary: QuAC is a modular approach for quantifying the correctness of service-oriented software systems. We present an implementation of QuAC for Java using the modeling tool Palladio and the deductive verification tool KeY.
• Score: 41.375461087536294
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Most formal methods see the correctness of a software system as a binary decision. However, proving the correctness of complex systems completely is difficult because they are composed of multiple components, usage scenarios, and environments. We present QuAC, a modular approach for quantifying the correctness of service-oriented software systems by combining software architecture modeling with deductive verification. Our approach is based on a model of the service-oriented architecture and the probabilistic usage scenarios of the system. The correctness of a single service is approximated by a coverage region, which is a formula describing which inputs for that service are proven to not lead to an erroneous execution. The coverage regions can be determined by a combination of various analyses, e.g., formal verification, expert estimations, or testing. The coverage regions and the software model are then combined into a probabilistic program. From this, we can compute the probability that under a given usage profile no service is called outside its coverage region. If the coverage region is large enough, then instead of attempting to get 100% coverage, which may be prohibitively expensive, run-time verification or testing approaches may be used to deal with inputs outside the coverage region. We also present an implementation of QuAC for Java using the modeling tool Palladio and the deductive verification tool KeY. We demonstrate its usability by applying it to a software simulation of an energy system.

Related papers

• SKADA-Bench: Benchmarking Unsupervised Domain Adaptation Methods with Realistic Validation [55.87169702896249]
  Unsupervised Domain Adaptation (DA) consists of adapting a model trained on a labeled source domain to perform well on an unlabeled target domain with some data distribution shift. We propose a framework to evaluate DA methods and present a fair evaluation of existing shallow algorithms, including reweighting, mapping, and subspace alignment. Our benchmark highlights the importance of realistic validation and provides practical guidance for real-life applications.
  arXiv  Detail & Related papers  (2024-07-16T12:52:29Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Discovering Decision Manifolds to Assure Trusted Autonomous Systems [0.0]
  We propose an optimization-based search technique for capturing the range of correct and incorrect responses a system could exhibit. This manifold provides a more detailed understanding of system reliability than traditional testing or Monte Carlo simulations. In this proof-of-concept, we apply our method to a software-in-the-loop evaluation of an autonomous vehicle.
  arXiv  Detail & Related papers  (2024-02-12T16:55:58Z)
• Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking [2.9129603096077332]
  We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. We have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker.
  arXiv  Detail & Related papers  (2023-11-09T11:25:24Z)
• Path Structured Multimarginal Schr\"odinger Bridge for Probabilistic Learning of Hardware Resource Usage by Control Software [1.7601096935307592]
  The solution of the path structured multimarginal Schr"odinger bridge problem (MSBP) is the most-likely measure-valued trajectory. We leverage recent algorithmic advances in solving such MSBPs for learning hardware resource usage by control software.
  arXiv  Detail & Related papers  (2023-10-01T07:35:12Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
  arXiv  Detail & Related papers  (2023-01-05T18:18:46Z)
• Satellite Image Time Series Analysis for Big Earth Observation Data [50.591267188664666]
  This paper describes sits, an open-source R package for satellite image time series analysis using machine learning. We show that this approach produces high accuracy for land use and land cover maps through a case study in the Cerrado biome.
  arXiv  Detail & Related papers  (2022-04-24T15:23:25Z)
• PDC-Net+: Enhanced Probabilistic Dense Correspondence Network [161.76275845530964]
  Enhanced Probabilistic Dense Correspondence Network, PDC-Net+, capable of estimating accurate dense correspondences. We develop an architecture and an enhanced training strategy tailored for robust and generalizable uncertainty prediction. Our approach obtains state-of-the-art results on multiple challenging geometric matching and optical flow datasets.
  arXiv  Detail & Related papers  (2021-09-28T17:56:41Z)
• Probabilistic Case-based Reasoning for Open-World Knowledge Graph Completion [59.549664231655726]
  A case-based reasoning (CBR) system solves a new problem by retrieving cases' that are similar to the given problem. In this paper, we demonstrate that such a system is achievable for reasoning in knowledge-bases (KBs) Our approach predicts attributes for an entity by gathering reasoning paths from similar entities in the KB.
  arXiv  Detail & Related papers  (2020-10-07T17:48:12Z)

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.