Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber, Robert Heinrich, Alexander Weigl

TL;DR

QuAC tackles the challenge that formal verification traditionally yields binary outcomes and scales poorly to complex, component-based systems. The approach combines architecture modeling (PCM) with formal source-code analysis (KeY) to define coverage regions for each service, then embeds these regions into the architectural model and uses probabilistic model counting to compute a coverage probability, which under-approximates the program's overall correctness probability under a given usage profile. Coverage regions can be obtained via formal verification, testing, expert estimates, or runtime monitoring, enabling incremental, modular refinement that blends static verification with run-time verification. The implementation on Java using PCM and KeY demonstrates feasibility, with a running energy-system case study illustrating how coverage regions influence the probability of safe execution; the work also discusses limitations (e.g., synchronous calls, single usage profile, absence of unbounded loops) and outlines directions for expanding to more general properties and security-focused analyses.

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.

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

TL;DR

QuAC tackles the challenge that formal verification traditionally yields binary outcomes and scales poorly to complex, component-based systems. The approach combines architecture modeling (PCM) with formal source-code analysis (KeY) to define coverage regions for each service, then embeds these regions into the architectural model and uses probabilistic model counting to compute a coverage probability, which under-approximates the program's overall correctness probability under a given usage profile. Coverage regions can be obtained via formal verification, testing, expert estimates, or runtime monitoring, enabling incremental, modular refinement that blends static verification with run-time verification. The implementation on Java using PCM and KeY demonstrates feasibility, with a running energy-system case study illustrating how coverage regions influence the probability of safe execution; the work also discusses limitations (e.g., synchronous calls, single usage profile, absence of unbounded loops) and outlines directions for expanding to more general properties and security-focused analyses.

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.
Paper Structure (37 sections, 3 theorems, 1 equation, 6 figures, 1 table)

This paper contains 37 sections, 3 theorems, 1 equation, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivation
  3. Contribution
  4. Limitations
  5. Preliminaries
  6. Architecture and code
  7. Software modeling with the Palladio Component Model
  8. Source code analysis
  9. Theoretical Overview of Quac
  10. Modeling the System
  11. Modeling a service
  12. Coverage regions
  13. Behavioral specifications
  14. Example
  15. Approximating the Correctness Probability
  16. ...and 22 more sections

Key Result

theorem 1

Let $\mathcal{U}$ a usage profile. Let $S, S'$ be sets of service models s.t. for each service $\mathit{s}$ the coverage region in $S$ for $\mathit{s}$ is smaller or equal to the corresponding one in $S'$. Then $Pr( \lightning \mid \llbracket \mathcal{U}(S)\rrbracket) \geq Pr(\lightning\mid \llbrack

Figures (6)

  • Figure 1: An overview of the Quac workflow.
  • Figure 2: An example software architecture and implementation.
  • Figure 3: Behavioral specifications for the services from \ref{['fig:example']}.
  • Figure 4: Probabilistic program corresponding to \ref{['fig:example']}.
  • Figure 5: Class diagram for the case study.
  • ...and 1 more figures

Theorems & Definitions (11)

  • definition 1: Service model
  • definition 2: Errors and correctness regions
  • definition 3: Correct coverage regions
  • definition 4: Usage profile
  • definition 5: Semantics of usage profile
  • theorem 1
  • proof
  • theorem 2: Local Contract Satisfaction
  • proof
  • corollary 1: Open Branches as Correct Coverage Region
  • ...and 1 more