More Web Proxy on the site http://driver.im/

research-article

Genetic Algorithm for Generating Counterexample in Stochastic Model Checking

Authors:

Tingting Zheng,

Yang LiuAuthors Info & Claims

ICNCC '18: Proceedings of the 2018 VII International Conference on Network, Communication and Computing

Pages 92 - 96

https://doi.org/10.1145/3301326.3301348

Published: 14 December 2018 Publication History

Abstract

Counterexamples are the most effective feature to convince system engineers about the value of formal verification. Generating the smallest counterexample in stochastic model checking has been proved to be NP-complete. In this paper, we apply the genetic algorithm to generate a counterexample for stochastic model checking. We use the diagnostic subgraph to represent a counterexample and employs indirect coding method to generate the more effective path. We implemented our method based on the stochastic model checker PRISM and applied it to some cases, in order to illustrate its applicability.

References

[1]

Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Proc. of CAV. Volume 6806 of LNCS (2011) 585--591.

Digital Library

[2]

Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2) (2011) 90--104.

Digital Library

[3]

H. Aljazzar, H. Hermanns, and S. Leue, "Counterexamples for Timed Probabilistic Reachability," Proc.Third Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 177--195, 2005.

Digital Library

[4]

H. Aljazzar and S. Leue, "Extended Directed Search for Probabilistic Timed Reachability," Proc. Fourth Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 33--51, 2006.

Digital Library

[5]

T. Han, J.-P. Katoen, and B. Damman, "Counterexample Generation in stochastic model checking," IEEE Trans. Software Eng., vol. 35, no. 2, pp. 241--257, Mar./Apr. 2009.

Digital Library

[6]

E. Abraham et al., Counterexample generation for discrete-time Markov models: An introductory survey, in Int. School Formal Methods for the Design of Computer Communication and Software Systems (Springer International, 2014), pp. 65--121.

Digital Library

[7]

Víctor M. Jiménez and Andrés Marzal. Computing the k shortest paths: A new algorithm and an experimental comparison. In Proc. of WAE), volume 1668 of LNCS, pages 15--29. Springer, 1999.

Digital Library

[8]

Husain Aljazzar and Stefan Leue. K*: A heuristic search algorithm for finding the k shortest paths. Artificial Intelligence, 175(18):2129--2154, 2011.

Digital Library

[9]

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. Advances in Computers, 58:118--149, 2003.

[10]

Miguel E. Andrés, Pedro D'Argenio, and Peter van Rossum. Significant diagnostic counterexamples in stochastic model checking. In Proc. of HVC, volume 5394 of LNCS, pages 129--148. Springer, 2008.

Digital Library

[11]

Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Transactions on Software Engineering 36(1) (2010) 37--60.

Digital Library

[12]

Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue, and Dimitar Simeonov. DiPro-A tool for probabilistic counterexample generation. In Proc. of SPIN, volume 6823 of LNCS, pages 183--187. Springer, 2011.

Digital Library

[13]

Chadha, R., Viswanathan, M.: A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Transactions on ComputationalLogic 12(1) (2010) 1--45.

Digital Library

[14]

Braitling, B., Wimmer, R., Becker, B., Jansen, N., Abrahám, E.:Counterexample generation for Markov chains using SMT-based bounded model checking. In:Proc. of FMOODS/FORTE. IFIP Advances in Information and Communication Technology, Springer (2011).

Digital Library

[15]

Wimmer, R., Becker, B., Jansen, N., Abrahám, E., Katoen, J.P.: Minimal critical subsystems for discrete-time Markov models. In: Proc. of TACAS. Volume 7214 of LNCS, Springer (2012) 299--314.

Digital Library

[16]

P. Godefroid and S. Khurshid, Exploring very large state spaces using genetic algorithms, Int. J. Softw. Tools Technol. Transf. 6(2) (2004) 117--127.

Digital Library

[17]

L. Benini et al., Policy optimization for dynamic power management, IEEE Trans.Comput.-Aided Des. Integr. Circuits Syst. 18(6) (1999) 813--833.

Digital Library

[18]

A. Itai and M. Rodeh, Symmetry breaking in distributed networks, Inf. Comput. 88(1) (1990) 60--87.

Digital Library

Cited By

Nejati FAbdul Hamid NKoohi SZadeh Z(2023)An Incremental Optimization Algorithm for Efficient Verification of Graph Transformation SystemsIEEE Access10.1109/ACCESS.2023.329141211(75748-75760)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3291412
Liu YMa YYang YZheng T(2021)Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical SystemsMicromachines10.3390/mi1209105912:9(1059)Online publication date: 31-Aug-2021
https://doi.org/10.3390/mi12091059
Nejati FGhani AYap NJafaar A(2021)Handling State Space Explosion in Component-Based Software Verification: A ReviewIEEE Access10.1109/ACCESS.2021.30817429(77526-77544)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3081742

Index Terms

Genetic Algorithm for Generating Counterexample in Stochastic Model Checking
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

A three-valued model abstraction framework for PCTL* stochastic model checking
Abstract
Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from ...
Scalable distributed on-the-fly symbolic model checking

This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. ...
Fluid model checking
CONCUR'12: Proceedings of the 23rd international conference on Concurrency Theory

In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ICNCC '18: Proceedings of the 2018 VII International Conference on Network, Communication and Computing

December 2018

372 pages

ISBN:9781450365536

DOI:10.1145/3301326

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 December 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

ICNCC 2018

ICNCC 2018: 2018 VII International Conference on Network, Communication and Computing

December 14 - 16, 2018

Taipei City, Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
53
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nejati FAbdul Hamid NKoohi SZadeh Z(2023)An Incremental Optimization Algorithm for Efficient Verification of Graph Transformation SystemsIEEE Access10.1109/ACCESS.2023.329141211(75748-75760)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3291412
Liu YMa YYang YZheng T(2021)Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical SystemsMicromachines10.3390/mi1209105912:9(1059)Online publication date: 31-Aug-2021
https://doi.org/10.3390/mi12091059
Nejati FGhani AYap NJafaar A(2021)Handling State Space Explosion in Component-Based Software Verification: A ReviewIEEE Access10.1109/ACCESS.2021.30817429(77526-77544)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3081742

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents