×

Quantifying software reliability via model-counting. (English) Zbl 1491.68113

Abate, Alessandro (ed.) et al., Quantitative evaluation of systems. 18th international conference, QEST 2021, Paris, France, August 23–27, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12846, 59-79 (2021).
Summary: 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 model-counters. We show the feasibility of our pipeline and benefits against competitors.
For the entire collection see [Zbl 1482.68004].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Avizienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. Inst. Syst. Res. 0114, 10 (2001). doi:10.1016/S0005-1098(00)00082-0, http://drum.lib.umd.edu/handle/1903/5952
[2] Biere, A.: runlim. Website (2016). http://fmv.jku.at/runlim
[3] Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 3569-3576. IJCAI/AAAI Press (2016). http://www.ijcai.org/Abstract/16/503
[4] Chen, Y-F; Hong, C-D; Sinha, N.; Wang, B-Y; Baier, C.; Tinelli, C., Commutativity of reducers, Tools and Algorithms for the Construction and Analysis of Systems, 131-146 (2015), Heidelberg: Springer, Heidelberg
[5] Clarke, E.; Kroening, D.; Lerda, F.; Jensen, K.; Podelski, A., A tool for checking ANSI-C programs, Tools and Algorithms for the Construction and Analysis of Systems, 168-176 (2004), Heidelberg: Springer, Heidelberg · Zbl 1126.68470
[6] Dimovski, AS; Legay, A., Computing program reliability using forward-backward precondition analysis and model counting, Fundamental Approaches to Software Engineering, 182-202 (2020), Cham: Springer, Cham
[7] Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic PathFinder. In: Proceedings - International Conference on Software Engineering, pp. 622-631 (2013). doi:10.1109/ICSE.2013.6606608
[8] Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, pp. 166-176. ACM (2012). doi:10.1145/2338965.2336773
[9] Hechter, M., Fichter, J.K.: Model Counting Competition 2020. Website (2020). https://mccompetition.org/. Accessed 5 Dec 2020
[10] Jasper, M.; Mues, M.; Schlüter, M.; Steffen, B.; Howar, F.; Margaria, T.; Steffen, B., RERS 2018: CTL, LTL, and reachability, Leveraging Applications of Formal Methods, Verification and Validation. Verification, 433-447 (2018), Cham: Springer, Cham
[11] Klebanov, V.; Manthey, N.; Muise, C.; Joshi, K.; Siegle, M.; Stoelinga, M.; D’Argenio, PR, SAT-based analysis and quantification of information flow in programs, Quantitative Evaluation of Systems, 177-192 (2013), Heidelberg: Springer, Heidelberg
[12] Klebanov, V., Weigl, A., Weisbarth, J.: Sound probabilistic #SAT with projection. In: Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 227, pp. 15-29 (2016). doi:10.4204/EPTCS.227.2
[13] Liu, S., Zhang, J.: Program analysis: From qualitative analysis to quantitative analysis. In: Proceedings - International Conference on Software Engineering, pp. 956-959 (2011). doi:10.1145/1985793.1985957
[14] Loera, JAD; Hemmecke, R.; Tauzer, J.; Yoshida, R., Effective lattice point counting in rational convex polytopes, J. Symb. Comput., 38, 4, 1273-1302 (2004) · Zbl 1137.52303
[15] Meel, K.S., Akshay, S.: Sparse hashing for scalable approximate model counting: theory and practice. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS 2020: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, 8-11 July 2020, pp. 728-741. ACM (2020). doi:10.1145/3373718.3394809 · Zbl 07299508
[16] Orso, A., Rothermel, G.: Software testing: a research travelogue (2000-2014). In: Future of Software Engineering, FOSE 2014 - Proceedings, pp. 117-132 (2014). doi:10.1145/2593882.2593885
[17] Sharma, S., Roy, S., Soos, M., Meel, K.S.: GANAK: a scalable probabilistic exact model counter. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10-16 August 2019, pp. 1169-1176. ijcai.org (2019). doi:10.24963/ijcai.2019/163
[18] Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, 27 January-1 February 2019, pp. 1592-1599. AAAI Press (2019). doi:10.1609/aaai.v33i01.33011592
[19] SoSy-Lab LMU: SV-Benchmarks (2020). https://github.com/sosy-lab/sv-benchmarks
[20] Stout, B.: C Snippets (2009). http://web.archive.org/web/20101204075132/c.snippets.org/
[21] Teuber, S., Weigl, A.: Evaluated artifact for “quantifying software reliability via model-counting” (2021). doi:10.5445/IR/1000134169
[22] Thurley, M.; Biere, A.; Gomes, CP, sharpSAT - counting models with advanced component caching and implicit BCP, Theory and Applications of Satisfiability Testing - SAT 2006, 424-429 (2006), Heidelberg: Springer, Heidelberg
[23] Visser, W., Bjørner, N., Shankar, N.: Software engineering and automated deduction. In: Herbsleb, J.D., Dwyer, M.B. (eds.) Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, 31 May-7 June 2014, pp. 155-166. ACM (2014). doi:10.1145/2593882.2593899
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.