Skip to main content
SpringerLink
Log in

Statistical Model Checking with Change Detection

  • Chapter
  • First Online:
Transactions on Foundations for Mastering Change I

Part of the book series: Lecture Notes in Computer Science ((TFMC,volume 9960))

Abstract

Statistical Model Checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result by using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows to approximate undecidable queries. The approach has been implemented in several toolsets such as Plasma Lab, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. In this paper, we add two new modest contributions to the cathedral of results on SMC. The first contribution is an algorithm that can be used to monitor changes in the probability distribution to satisfy a bounded-time property at runtime. Concretely, the algorithm constantly monitors the execution of the deployed system, and raises a flag when it observes that the probability has changed significantly. This is done by extending the applicability of the CUSUM algorithm used in signal processing into the formal validation setting. Our second contribution is to show how the programming interface of Plasma Lab can be exploited in order to make SMC technology directly available in toolsets used by designers. This integration is done by exploiting simulation facilities of design tools. Our approach thus differs from the one adopted by other SMC/formal verification toolsets which assume the existence of formal semantics for the design language, as well as a compiling chain to the rather academic one used by validation tool. The concept results in the integration of Plasma Lab as a library of the Simulink toolset. The contributions are illustrated by using Plasma Lab to verify a Simulink case study modelling a pig shed temperature controller.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://project.inria.fr/plasma-lab/examples/fault-tolerant-fuel-control-system/.

  2. 2.

    Available at https://project.inria.fr/plasma-lab/.

  3. 3.

    https://project.inria.fr/plasma-lab/documentation/tutorial/igrida-experimentation/.

  4. 4.

    https://code.google.com/p/matlabcontrol/.

References

  1. Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electron. Notes Theoret. Comput. Sci. 109, 43–56 (2004)

    Article  MATH  Google Scholar 

  2. Barnat, J., Beran, J., Brim, L., Kratochvíla, T., Ročkai, P.: Tool chain to support automated formal verification of avionics simulink designs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 78–92. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32469-7_6

    Chapter  Google Scholar 

  3. Basseville, M., Nikiforov, I.V.: Detection of Abrupt Changes: Theory and Application. Prentice-Hall Inc., Englewood Cliffs (1993)

    Google Scholar 

  4. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Int. J. Softw. Tools Technol. Transf. 14(1), 53–72 (2012)

    Article  Google Scholar 

  5. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an AFDX infrastructure using simulations and probabilities. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 330–344. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_25

    Chapter  Google Scholar 

  6. Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 128–137. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02017-9_16

    Chapter  Google Scholar 

  7. Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. 2(5) (2006). http://dx.doi.org/10.2168/LMCS-2(5:5)2006

  8. 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

    Chapter  Google Scholar 

  9. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_29

    Chapter  Google Scholar 

  10. Clarke, E., Donzé, A., Legay, A.: Statistical Model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2009). doi:10.1007/978-3-642-01702-5_16

    Chapter  Google Scholar 

  11. Clarke, E., Donzé, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods Syst. Des. 36(2), 97–113 (2010)

    Article  MATH  Google Scholar 

  12. Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in BioLab: applications to the automated analysis of T-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. Lecture Notes in Artificial Intelligence (LNAI), vol. 5307, pp. 231–250. Springer, Heidelberg (2008). doi:10.1007/978-3-540-88562-7_18

    Chapter  Google Scholar 

  13. D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469–484 (2015)

    Article  Google Scholar 

  14. David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Proceedings of the 1st International Workshop on Hybrid Systems and Biology (HSB), EPTCS, vol. 92, pp. 122–136 (2012)

    Google Scholar 

  15. David, A., Du, D., Guldstrand Larsen, K., Legay, A., Mikučionis, M.: Optimizing control strategy using statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 352–367. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_24

    Chapter  Google Scholar 

  16. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_7

    Chapter  Google Scholar 

  17. 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

    Chapter  Google Scholar 

  18. Bhatt, D., Madl, G., Oglesby, D., Schloegel, K.: Towards scalable verification of commercial avionics software. In: AIAA Infotech@Aerospace 2010. Infotech@Aerospace Conferences, American Institute of Aeronautics and Astronautics, April 2010

    Google Scholar 

  19. Grabiec, B., Traonouez, L.-M., Jard, C., Lime, D., Roux, O.H.: Diagnosis using unfoldings of parametric time petri nets. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 137–151. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15297-9_12

    Chapter  Google Scholar 

  20. 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

    Chapter  Google Scholar 

  21. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  22. Höfner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 322–336. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_22

    Chapter  Google Scholar 

  23. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_8

    Chapter  Google Scholar 

  24. Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_38

    Chapter  Google Scholar 

  25. Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using Uppaal Tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227–240. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75454-1_17

    Chapter  Google Scholar 

  26. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03845-7_15

    Chapter  Google Scholar 

  27. Kim, Y., Kim, M., Kim, T.-H.: Statistical model checking for safety critical hybrid systems: an empirical evaluation. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 162–177. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39611-3_18

    Chapter  Google Scholar 

  28. Koh, C.H., Palaniappan, S.K., Thiagarajan, P., Wong, L.: Improved statistical model checking methods for pathway analysis. BMC Bioinf. 13(17), 1–12 (2012)

    Google Scholar 

  29. 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

    Chapter  Google Scholar 

  30. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  31. Mathworks: polyspace a static analysis tools for C/C++ and Ada, December 2014. http://www.mathworks.fr/products/polyspace/

  32. Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006). doi:10.1007/11901433_33

    Chapter  Google Scholar 

  33. Page, E.S.: Continuous inspection schemes. Biometrika 41(1/2), 100–115 (1954). http://www.jstor.org/stable/2333009

    Article  MathSciNet  MATH  Google Scholar 

  34. Prover: Prover-Plugin, December 2014. http://www.prover.com/products/prover_plugin/

  35. 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

    Chapter  Google Scholar 

  36. Verdier, G., Hilgert, N., Vila, J.: Adaptive threshold computation for CUSUM-type procedures in change detection and isolation problems. Comput. Stat. Data Anal. 52(9), 4161–4174 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  37. Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)

    Article  MathSciNet  MATH  Google Scholar 

  38. Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)

    Google Scholar 

  39. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Des. 43(2), 338–367 (2013)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria Rennes – Bretagne Atlantique, 263 Avenue du Général Leclerc - Bât 12, Rennes, France

    Axel Legay & Louis-Marie Traonouez

Authors
  1. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Louis-Marie Traonouez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Louis-Marie Traonouez .

Editor information

Editors and Affiliations

  1. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this chapter

Cite this chapter

Legay, A., Traonouez, LM. (2016). Statistical Model Checking with Change Detection. In: Steffen, B. (eds) Transactions on Foundations for Mastering Change I. Lecture Notes in Computer Science(), vol 9960. Springer, Cham. https://doi.org/10.1007/978-3-319-46508-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46508-1_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46507-4

  • Online ISBN: 978-3-319-46508-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation