Partial Order Methods for Statistical Model Checking and Simulation
International audience Statistical model checking has become a promising technique to circumvent the state space explosion problem in model-based verification. It trades time for memory, via a probabilistic simulation and exploration of the model behaviour—often combined with effective a posteriori...
Main Authors: | , , , |
---|---|
Other Authors: | , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
Online Access: | https://hal.inria.fr/hal-01583327 https://hal.inria.fr/hal-01583327/document https://hal.inria.fr/hal-01583327/file/978-3-642-21461-5_4_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_4 |
id |
ftifiphal:oai:HAL:hal-01583327v1 |
---|---|
record_format |
openpolar |
spelling |
ftifiphal:oai:HAL:hal-01583327v1 2023-05-15T16:49:48+02:00 Partial Order Methods for Statistical Model Checking and Simulation Bogdoll, Jonathan Ferrer Fioriti, Luis, Hartmanns, Arnd Hermanns, Holger Saarland University Saarbrücken Roberto Bruni Juergen Dingel TC 6 WG 6.1 Reykjavik,, Iceland 2011-06-06 https://hal.inria.fr/hal-01583327 https://hal.inria.fr/hal-01583327/document https://hal.inria.fr/hal-01583327/file/978-3-642-21461-5_4_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_4 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_4 hal-01583327 https://hal.inria.fr/hal-01583327 https://hal.inria.fr/hal-01583327/document https://hal.inria.fr/hal-01583327/file/978-3-642-21461-5_4_Chapter.pdf doi:10.1007/978-3-642-21461-5_4 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583327 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.59-74, ⟨10.1007/978-3-642-21461-5_4⟩ [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftifiphal https://doi.org/10.1007/978-3-642-21461-5_4 2023-03-21T20:40:06Z International audience Statistical model checking has become a promising technique to circumvent the state space explosion problem in model-based verification. It trades time for memory, via a probabilistic simulation and exploration of the model behaviour—often combined with effective a posteriori hypothesis testing. However, as a simulation-based approach, it can only provide sound verification results if the underlying model is a stochastic process. This drastically limits its applicability in verification, where most models are indeed variations of nondeterministic transition systems. In this paper, we describe a sound extension of statistical model checking to scenarios where nondeterminism is present. We focus on probabilistic automata, and discuss how partial order reduction can be twisted such as to apply statistical model checking to models with spurious nondeterminism. We report on an implementation of this technique and on promising results in the context of verification and dependability analysis of distributed systems. Conference Object Iceland IFIP Open Digital Library (International Federation for Information Processing) 59 74 |
institution |
Open Polar |
collection |
IFIP Open Digital Library (International Federation for Information Processing) |
op_collection_id |
ftifiphal |
language |
English |
topic |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
spellingShingle |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Bogdoll, Jonathan Ferrer Fioriti, Luis, Hartmanns, Arnd Hermanns, Holger Partial Order Methods for Statistical Model Checking and Simulation |
topic_facet |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
description |
International audience Statistical model checking has become a promising technique to circumvent the state space explosion problem in model-based verification. It trades time for memory, via a probabilistic simulation and exploration of the model behaviour—often combined with effective a posteriori hypothesis testing. However, as a simulation-based approach, it can only provide sound verification results if the underlying model is a stochastic process. This drastically limits its applicability in verification, where most models are indeed variations of nondeterministic transition systems. In this paper, we describe a sound extension of statistical model checking to scenarios where nondeterminism is present. We focus on probabilistic automata, and discuss how partial order reduction can be twisted such as to apply statistical model checking to models with spurious nondeterminism. We report on an implementation of this technique and on promising results in the context of verification and dependability analysis of distributed systems. |
author2 |
Saarland University Saarbrücken Roberto Bruni Juergen Dingel TC 6 WG 6.1 |
format |
Conference Object |
author |
Bogdoll, Jonathan Ferrer Fioriti, Luis, Hartmanns, Arnd Hermanns, Holger |
author_facet |
Bogdoll, Jonathan Ferrer Fioriti, Luis, Hartmanns, Arnd Hermanns, Holger |
author_sort |
Bogdoll, Jonathan |
title |
Partial Order Methods for Statistical Model Checking and Simulation |
title_short |
Partial Order Methods for Statistical Model Checking and Simulation |
title_full |
Partial Order Methods for Statistical Model Checking and Simulation |
title_fullStr |
Partial Order Methods for Statistical Model Checking and Simulation |
title_full_unstemmed |
Partial Order Methods for Statistical Model Checking and Simulation |
title_sort |
partial order methods for statistical model checking and simulation |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
https://hal.inria.fr/hal-01583327 https://hal.inria.fr/hal-01583327/document https://hal.inria.fr/hal-01583327/file/978-3-642-21461-5_4_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_4 |
op_coverage |
Reykjavik,, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://hal.inria.fr/hal-01583327 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.59-74, ⟨10.1007/978-3-642-21461-5_4⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_4 hal-01583327 https://hal.inria.fr/hal-01583327 https://hal.inria.fr/hal-01583327/document https://hal.inria.fr/hal-01583327/file/978-3-642-21461-5_4_Chapter.pdf doi:10.1007/978-3-642-21461-5_4 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_4 |
container_start_page |
59 |
op_container_end_page |
74 |
_version_ |
1766039980900089856 |