KIT | KIT-Bibliothek | Impressum | Datenschutz

Quantifying Software Reliability via Model-Counting

Teuber, Samuel; Weigl, Alexander ORCID iD icon


Critical software should be verified. But how to handle the situation when a proof for the functional correctness could not be established? In this case, an assessment of the software is required to estimate the risk of using the software. In this paper, we contribute to the assessment of critical software with a formal approach to measure the reliability of the software against its functional specification. We support bounded C-programs precisely where the functional specification is given as assumptions and assertions within the source code. We count and categorize the various program runs to compute the reliability as the ratio of failing program runs (violating an assertion) to all terminating runs. Our approach consists of a preparing program translation, the reduction of C-program into SAT instances via software-bounded model-checker (cbmc), and precise or approximate model-counting providing a reliable assessment. We evaluate our prototype implementation on over 24 examples with different modelcounters. We show the feasibility of our pipeline and benefits against competitors.

Postprint §
DOI: 10.5445/IR/1000138400
Veröffentlicht am 20.08.2022
DOI: 10.1007/978-3-030-85172-9_4
Zitationen: 1
Zitationen: 3
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2021
Sprache Englisch
Identifikator ISSN: 0302-9743, 1611-3349
KITopen-ID: 1000138400
HGF-Programm 46.23.01 (POF IV, LK 01) Methods for Engineering Secure Systems
Erschienen in Quantitative Evaluation of Systems: 18th International Conference, QEST 2021, Paris, France, August 23–27, 2021, Proceedings. Ed.: A. Abate
Veranstaltung 18th International Conference on the Quantitative Evaluation of Systems (QEST 2021), Online, 23.08.2021 – 27.08.2021
Verlag Springer Verlag
Seiten 59-79
Serie Lecture Notes in Computer Science (LNCS) ; 12846
Vorab online veröffentlicht am 19.08.2021
Schlagwörter software verification, software reliability, model counting
Nachgewiesen in Dimensions
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page