Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

Reviewed Paper In Proceedings

Author(s):Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber, Robert Heinrich, and Alexander Weigl
In:Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024
Publisher:Association for Computing Machinery (ACM)
Series:SAC '24
Year:2024
Pages:1702-1711
PDF:
URL:https://doi.org/10.1145/3605098.3636008
DOI:10.1145/3605098.3636008
Keywords: service-oriented architecture component-based architecture architecture modeling deductive verification quantitative verification architecture simulation software reliability estimation

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. 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.

BibTeX

@InProceedings{QuACSAC2024,
  author    = {Florian Lanzinger and
               Christian Martin and
               Frederik Reiche and
               Samuel Teuber and
               Robert Heinrich and
               Alexander Weigl},
  title     = {Quantifying Software Correctness by Combining Architecture Modeling
               and Formal Program Analysis},
  year      = {2024},
  month     = may,
  editor    = {Jiman Hong and
               Juw Won Park},
  publisher = {Association for Computing Machinery (ACM)},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/3605098.3636008},
  doi       = {10.1145/3605098.3636008},
  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. 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.},
  booktitle = {Proceedings of the 39th {ACM/SIGAPP} Symposium on Applied Computing,
               {SAC} 2024},
  pages     = {1702--1711},
  numpages  = {10},
  keywords  = {service-oriented architecture, component-based architecture,
               architecture modeling, deductive verification, quantitative
               verification, architecture simulation, software reliability
               estimation},
  location  = {Avila, Spain},
  series    = {SAC '24},
  pdf       = {PDF:/lanzinger/pdf/QuACSAC2024.pdf}
}