Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Computing
Published in: Computing 2/2023

09-11-2022 | Regular Paper

Constraint-based debugging in probabilistic model checking

Author: Hichem Debbi

Published in: Computing | Issue 2/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A counterexample in model checking is an error trace that represents a valuable tool for debugging. In Probabilistic Model Checking (PMC), the counterexample generation has a quantitative aspect. A probabilistic counterexa mple is a set of diagnostic paths in which a path formula holds, and whose probability mass violates the probability threshold. Comparing to conventional model checking, debugging and analyzing counterexamples in PMC is a very complex task. In this paper, we propose a debugging method for Markov models described in the probabilistic model checker PRISM by analyzing probabilistic counterexamples. The probabilistic counterexample generated is subjected to a set of assertions, which are employed for detecting incorrect behavior of the model, and thus locating the erroneous transitions contributing to the error. Our method has been implemented and tested on many PRISM models of different case studies. The method shows promising results in terms of execution time as well as its efficiency in locating the erroneous transitions.
previous article Algorithms for path optimizations: a short survey
next article Time series-based workload prediction using the statistical hybrid model for the cloud environment

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now
Literature
1.
Beer I, Ben-David S, Chockler H, Orni A, Treer R (2012) Explaining counterexamples using causality. Formal Methods Syst Design 40(1):20–40CrossRefMATH
2.
Zeller A (1999) Yesterday, my program worked. today, it does not. why? In: ACM symposium on the foundations of software engineering, pp 253–267
3.
Wang C, Yang Z, Ivancic F, Gupta A (2006) Whodunit? causal analysis for counterexamples. In: 4th international symposium, ATVA. LNCS, vol 4218, Springer, Berlin, Heidelberg, pp 82–95
4.
Groce A (2005) Error Explanation and Fault Localization with Distance Metrics. PhD thesis, School of Computer Science, Carnegie Mellon University
5.
Hansson H, Jonsson B (1994) Logic for reasoning about time and reliability. Formal Asp Comput 6(5):512–535CrossRefMATH
6.
Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Log 1(1):162–170CrossRefMATH
7.
Baier C, Haverkort B, Hermanns H, Katoen JP (2003) Model checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(7):524–541CrossRefMATH
8.
Debbi H, Bourahla M (2013) Causal analysis of probabilistic counterexamples. In: Proceedings of the eleventh ACM-IEEE international conference on formal methods and models for codesign (Memocode), pp 77–86
9.
Debbi H (2016) Debugging of markov decision processes (mdps) models. In: Proceedings of the first workshop on causal reasoning for embedded and safety-critical systems, pp 25–39
10.
Wimmer R, Jansen N, Vorpahl A (2013) High-level counterexamples for probabilistic automata. In: Quantitative evaluation of systems (QEST). LNCS, vol 8054, Springer, Berlin, Heidelberg, pp 39–54
11.
Kleer J, Kurien J (2003) Fundamentals of model-based diagnosis. In: IFAC Proceedings Volumes, vol 36, Sciencedirect pp 25–36
12.
Wong WE, Gao R, Li Y, Abreu R, Wotawa F (2016) A survey on software fault localization. IEEE Trans Softw Eng 42(8):707–740CrossRef
13.
Nica M (2010) On the Use of Constraints in Automated Program Debugging - From Foundations to Empirical Results. PhD thesis, Graz University of Technology
14.
Friedrich G, Stumptner M, Wotawa F (1999) Model-based diagnosis of hardware designs. Artif Intell 111(1):3–39CrossRefMATH
15.
Ferrante J, Ottenstein K, Warren J (1987) The program dependence graph and its use in optimization. ACM Trans Program Lang Syst (TOPLAS) 9:319–349CrossRefMATH
16.
Weiser M (1981) Program slicing. In: Proceeding ICSE ’81 Proceedings of the 5th international conference on Software engineering, IEEE Press Piscataway, pp 439–449
17.
Millett L, Teitelbaum T (2000) Issues in slicing promela and its applications to model checking, protocol understanding, and simulation. Int J Softw Tools Technol Transfer 2:443–449CrossRef
18.
Hinton A, Kwiatkowska M, Norman G, Parker D (2006) Prism: a tool for automatic verification of probabilistic systems. In: Proceedings of TACAS, Springer, Berlin, Heidelberg, pp 441–444
19.
Aljazzar H, Leitner-Fischer F, Leue S, Simeonov D (2011) Dipro - a tool for probabilistic counterexample generation. In: Proceedings of the 18th international SPIN Workshop. LNCS 6823, Springer, Berlin, Heidelberg, pp 183–187
20.
Aljazzar H, Leue S (2010) Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans Softw Eng 36(1):37–60CrossRef
21.
Han T, Katoen J (2009) Counterexamples generation in probabilistic model checking. IEEE Trans Softw Eng 35(2):72–86MATH
22.
Clarke EM (2008) In: The birth of model checking. Springer-Verlag, pp 1–26
23.
Mayer W, Stumptner M, Wieland D, Wotawa F (2000) Can AI help to improve debugging substantially? debugging experiences with value-based models. In: Proceedings of the European conference on artificial intelligence (ECAI), IOS Press, pp 417–421
24.
Wotawa F, Nica M, Moraru I (2012) Automated debugging based on a constraint model of the program and a test case. J Logic Algebr Program 81(4):390–407CrossRefMATH
25.
Abreu R, Hofer B, Perez A, Wotawa F (2015) Using constraints to diagnose faulty spreadsheets. Softw Qual J 23(2):297–322CrossRef
26.
Wotawa F (2008) Bridging the gap between slicing and model-based diagnosis. In: Proceedings of the 20th international conference on software engineering and knowledge engineering (SEKE), pp 836–841
27.
Wotawa F (2002) On the relationship between model-based debugging and program slicing. Artif Intell 135:124–143CrossRefMATH
28.
29.
30.
Baah G, Podgurski A, Harrold MJ (2010) The probabilistic program dependence graph and its application to fault diagnosis. IEEE Trans Software Eng 36:528–545CrossRef
31.
Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: SIGPLAN Not, vol 43(6). pp 281–292
32.
Keng B, Veneris A (2012) Automated debugging of missing input constraints in a formal verification environment. In: Proceedings of the 12th conference on formal methods in computer-aided design (FMCAD 2012), IEEE, pp 101–105
33.
Collavizza H, Vinh NL, Rueher M, Devulder S, Gueguen T (2011) A dynamic constraint-based bmc strategy for generating counterexamples. In: Proceedings of the 2011 ACM symposium on applied computing. SAC ’11, pp 1633–1638
34.
Bekkouche M, Collavizza H, Rueher M (2015) Locfaults: a new flow-driven and constraint-based error localization approach. In: Proceedings of the 30th annual ACM symposium on applied computing. SAC ’15, New York, NY, USA, pp 1773–1780
35.
Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Chockler H, Weissenbacher G (eds) Computer aided verification. Springer, Cham, pp 270–288CrossRef
36.
Aljazzar H, Leue S (2009) Generation of counterexamples for model checking of markov decision processes. In: Proceedings of the international conference on quantitative evaluation of systems (QEST), pp 197–206
37.
Halpern J, Pearl J (2001) Causes and explanations: a structural-model approach part i: Causes. In: Proceedings of the 17th UAI, pp 194–202
38.
Chockler H, Halpern JY (2004) Responsibility and blame: a structural model approach. J Artif Intell Res (JAIR) 22(1):93–115CrossRefMATH
39.
Wimmer R, Jansen N, Abraham E, Becker B, Katoen J (2012) Minimal critical subsystems for discrete-time markov models. In: TACAS. LNCS, vol 7214, Springer, Berlin, Heidelberg, pp 299–314
40.
Leitner-Fischer F, Leue S (2013) Probabilistic fault tree synthesis using causality computation. Int J Crit Comput Based Syst 4(2):119–143CrossRef
41.
42.
Aljazzar H, Leue S (2011) K*: a heuristic search algorithm for finding the k shortest paths. Artif Intell 175(18):2129–2154CrossRefMATH
43.
Katoen JP, Khattri M, Zapreev IS (2005) A markov reward model checker. In: Proceedings of QEST. pp 243–244
44.
45.
Ibe O, Trivedi K (1990) Stochastic Petri net models of polling systems. IEEE J Sel Areas Commun 8:1649–1657CrossRef
46.
de Moura L, Bjørner N (2008) Z3: An efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin Heidelberg, pp 337–340CrossRef
47.
48.
49.
50.
51.
52.
53.
Fischer F, Leue S (2013) Causality checking for complex system models. In: Proceedings of verification, model checking, and abstract interpretation (VMCAI). LNCS 7737, Springer, Berlin, Heidelberg, pp 248–276
54.
Calinescu R, Češka M, Gerasimou S, Kwiatkowska M, Paoletti N (2018) Efficient synthesis of robust models for stochastic systems. J Syst Softw 143:140–158CrossRef
55.
Chatzieleftheriou G, Katsaros P (2018) Abstract model repair for probabilistic systems. Inf Comput 259:142–160CrossRefMATH
56.
Li X, Li W, Zhang Y, Zhang L (2019) Deepfl: integrating multiple fault diagnosis dimensions for deep fault localization. In: Proceedings of the 28th ACM SIGSOFT international symposium on software testing and analysis, pp 169–180
57.
Lou Y, Ghanbari A, Li X, Zhang L, Zhang H, Hao D, Zhang L (2020) Can automated program repair refine fault localization? a unified debugging approach. In: Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis. ISSTA 2020, pp 75–87
Metadata
Title
Constraint-based debugging in probabilistic model checking
Author
Hichem Debbi
Publication date
09-11-2022
Publisher
Springer Vienna
Published in
Computing / Issue 2/2023
Print ISSN: 0010-485X
Electronic ISSN: 1436-5057
DOI
https://doi.org/10.1007/s00607-022-01130-0

Other articles of this Issue 2/2023

Computing 2/2023 Go to the issue

Regular Paper

Community detection algorithms for recommendation systems: techniques and metrics

Regular Paper

Meddal: meeting deadlines and data locality via bin packing in cloud environment

Regular Paper

HaSGP: an effective graph partition method for heterogeneous-aware

Regular Paper

Influence maximization based on SATS scheme in social networks

Regular Paper

Microservice compositions based on the choreography of BPMN fragments: facing evolution issues

Regular Paper

Edge exploration of anonymous graph by mobile agent with external help

Premium Partner

    Image Credits