Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Statistical Model Checking: Past, Present, and Future

verfasst von : Kim G. Larsen, Axel Legay

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Statistical Model Checking (SMC) is a compromise between verification and testing where executions of the systems are monitored until an algorithm from statistics can produce an estimate for the system to satisfy a given property.
The objective of this introduction is to summarizes SMC as well as a series of challenges for which contributors at Isola propose a solution.
Contributions include new SMC toolsets, new flexible SMC algorithms for larger classes of systems, and new applications.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Erratum to: Leveraging Applications of Formal Methods, Verification and Validation (Part I)
Nächstes Kapitel Hypothesis Testing for Rare-Event Simulation: Limitations and Possibilities
Fußnoten
1
As we shall see later, stochastic systems may deal with additional quantities such as real-time.
 
2
This thesis is not concerned with the definition of efficient monitoring procedures.
 
Literatur
[A.99]
[AM]
Arora, S.: Panduranga Rao, M.V.: Probabilistic model checking of incomplete models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 62–76. Springer, Cham (2016)
[AvdP]
Ahmad, W., van de Pol, J.: Synthesizing energy-optimal controllers for multi-processor dataflow applications with uppaal. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 94–113. Springer, Cham (2016)
[BCCZ99]
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). doi:10.​1007/​3-540-49059-0_​14 CrossRef
[BCLS13]
Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40196-1_​12 CrossRef
[BCM+92]
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comp. 98(2), 142–170 (1992)MathSciNetCrossRefMATH
[BHHK03]
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)CrossRefMATH
[BJK+05]
Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)MATH
[BK08]
Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)MATH
[BMR05]
Ball, T., Millstein, T.D., Rajamani, S.K.: Polymorphic predicate abstraction. ACM Trans. Program. Lang. Syst. 27(2) (2005)
[Bry92]
Bryant, R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef
[CB06]
Ciesinski, F., Baier, C.: Liquor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proceedings of 3rd International Conference on the Quantitative Evaluation of Systems (QEST), pp. 131–132. IEEE (2006)
[CE81]
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.​1007/​BFb0025774 CrossRef
[CG04]
Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147–188. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-24611-4_​5 CrossRef
[CGP99]
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
[CV03]
Clarke, E., Veith, H.: Counterexamples revisited: principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 208–224. Springer, Heidelberg (2003). doi:10.​1007/​978-3-540-39910-0_​9 CrossRef
[CY95]
[DG07]
[DLL+11]
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​27 CrossRef
[DPP04]
Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theoret. Comput. Sci. 311(1–3), 221–256 (2004)MathSciNetCrossRefMATH
[FG05]
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110–121. ACM (2005)
[GPS02]
Cabodi, G., Camurati, P., Quer, S.: Can BDDs compete with sat solvers on bounded model checking? In: Proceedings of 39th Design Automation Conference (DAC), pp. 117–122. ACM (2002)
[HCZ11]
Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 144–160. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-19829-8_​10 CrossRef
[HR02]
Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). doi:10.​1007/​3-540-46002-0_​24 CrossRef
[JKO+07]
Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69–85. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-77966-7_​9 CrossRef
[JLL+]
Jegourel, C., Lukina, A., Legay, A., Smolka, S., Grosu, R., Bartocci, E.: Feedback control for statistical model checking of cyber-physical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 46–61. Springer, Cham (2016)
[KNP04]
Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: a tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)
[KNP11]
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
[Kre]
Kretinsky, J.: Survey of statistical verification of linear unbounded properties: model checking and distances. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 27–45. Springer, Cham (2016)
[LdPB]
Linard, A., de Paula Bueno, M.L.: Towards adaptive scheduling of maintenance for cyber-physical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 134–150. Springer, Cham (2016)
[LST]
Legay, A., Sedwards, S., Traonouez, L.-M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 77–93. Springer, Cham (2016)
[Oka59]
Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29–35 (1959)MathSciNetCrossRefMATH
[Pnu77]
Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)
[RdBS]
Reijsbergen, D., de Boer, P.-T., Scheinhardt, W.: Hypothesis testing for rare-event simulation: limitations and possibilities. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 16–26. Springer, Cham (2016)
[RS]
Ruijters, E., Stoelinga, M.: Better railway engineering through statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 151–165. Springer, Cham (2016)
[Str]
Strnadel, J.: On creation, analysis of reliability models by means of stochastic timed automata, statistical model checking: principle. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 166–181. Springer, Cham (2016)
[SVA04]
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-27813-9_​16 CrossRef
[SVA05]
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: CAV, pp. 266–280 (2005)
[tBLVL]
ter Beek, M., Legay, A., Vandin, A., Lafuente, A.L.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 114–133. Springer, Cham (2016)
[Wal45]
[WG93]
Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233–246. Springer, Heidelberg (1993). doi:10.​1007/​3-540-57208-2_​17
[You05a]
Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)
[You05b]
Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2005)
[You06]
Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 142–156. Springer, Heidelberg (2005). doi:10.​1007/​11609773_​10 CrossRef
[YS02]
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45657-0_​17 CrossRef
Metadaten
Titel
Statistical Model Checking: Past, Present, and Future
verfasst von
Kim G. Larsen
Axel Legay
Copyright-Jahr
2016
Buch
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

Print ISBN: 978-3-319-47165-5

Electronic ISBN: 978-3-319-47166-2

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-47166-2_1