@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} }
Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
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.