Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

@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}
}