Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Qualitative and quantitative analysis of safety-critical systems with

  • FMICS-AVoCS
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We give an overview of the (pronounced “safety sharp”) framework for rigorous, model-based analysis of safety-critical systems. We introduce ’s expressive modeling language based on the programming language, showing how ’s fault modeling and flexible model composition capabilities can be used to model a case study from the transportation sector with multiple design variants. A formal semantics for executable probabilistic models is given. Fully automated qualitative and quantitative safety analyses are conducted for the case study using algorithms of the model checkers LTSmin and MRMC. The results of the quantitative analyses are discussed in comparison with results obtained by using traditional techniques.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

References

  1. Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference Computer Aided Verification (CAV’04). Lecture Notes in Computer Science, vol. 3114, pp. 484–487. Springer (2004)

  2. Avižienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. Dependable Secur. Comput. 1(1), 11–33 (2004)

    Article  Google Scholar 

  3. Baier, C., Ciesinski, F., Größer, M.: PROBMELA: a modeling language for communicating probabilistic systems. In: Proceedings of the 2nd ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’2004). pp. 57–66. IEEE (2004)

  4. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  5. Batteux, M., Prosvirnova, T., Rauzy, A., Kloul, L.: The altaRica 3.0 project for model-based safety assessment. In: Industrial Informatics. pp. 741–746. IEEE (2013)

  6. Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V., Noll, T., Roveri, M.: The COMPASS Approach: correctness, modelling and performability of aerospace systems. In: Computer Safety, Reliability, and Security, pp. 173–186. Springer (2009)

  7. Butcher, J.: The Numerical Analysis of Ordinary Differential Equations: Runge-Kutta and General Linear Methods, 2nd edn. Wiley, Chichester, UK (2003)

  8. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an open source tool for symbolic model checking. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 2404, pp. 359–364. Springer (2002)

  9. Diez, D.M., Barr, C.D., Çetinkaya Rundel, M.: OpenIntro Statistics. OpenIntro, Inc., (2015)

  10. Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110–132 (2014)

    Article  Google Scholar 

  11. Habermaier, A.: Design Time and Run Time Formal Safety Analysis using Executable Models. Ph.D. thesis, University of Augsburg (2017)

  12. Habermaier, A., Eberhardinger, B., Seebach, H., Leupolz, J., Reif, W.: Runtime model-based safety analysis of self-organizing systems with S#. In: 2015 Self-Adaptive and Self-Organizing Systems Wsh.s. pp. 128–133. IEEE (2015)

  13. Habermaier, A., Güdemann, M., Ortmeier, F., Reif, W., Schellhorn, G.: The ForMoSA approach to qualitative and quantitative model-based safety analysis. In: Railway Safety, Reliability, and Security, pp. 65–114. IGI Global (2012)

  14. Habermaier, A., Knapp, A., Leupolz, J., Reif, W.: Fault-aware modeling and specification for efficient formal safety analysis. In: ter Beek et al.[32] , pp. 97–114

  15. Habermaier, A., Leupolz, J., Reif, W.: Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with S#. In: ter Beek et al. [32], pp. 150–167

  16. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)

    Article  Google Scholar 

  17. Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2004)

    Google Scholar 

  18. ISO: ISO/IEC 23270: Information technology – Programming languages –C#(2006)

  19. ISO: ISO 24765: Systems and software engineering – Vocabulary (2010)

  20. ISO: ISO/IEC 23271: Information technology – Common Language Infrastructure (2012)

  21. Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 9035, pp. 692–707. Springer (2015)

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

    Article  Google Scholar 

  23. Kirsch, C., Sengupta, R.: The evolution of real-time programming. In: Handbook of Real-Time and Embedded Systems, chap. CRC Press, (2007)

  24. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806, pp. 585–591. Springer (2011)

  25. Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Formal Methods in Computer Aided Design, pp. 247–255 (2010)

  26. Leveson, N.: Engineering a Safer World. MIT Press, Cambridge (2011)

    Google Scholar 

  27. Lipaczewski, M., Struck, S., Ortmeier, F.: Using tool-supported model based safety analysis – progress and experiences in SAML development. In: High-Assurance Systems Engineering, pp. 159–166. IEEE (2012)

  28. Noll, T.: Safety, dependability and performance analysis of aerospace systems. In: Formal Techniques for Safety-Critical Systems, CCIS, vol. 476, pp. 17–31. Springer (2015)

  29. Object Management Group: OMG Systems Modeling Language, Version 1.4 (2015)

  30. Ortmeier, F., Schellhorn, G., Thums, A., Reif, W., Hering, B., Trappschuh, H.: Safety analysis of the height control system for the Elbtunnel. In: Computer Safety, Reliability and Security, Lecture Notes in Computer Science, vol. 2434, pp. 296–308. Springer (2002)

  31. Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)

  32. ter Beek, M.H., Gnesi, S., Knapp, A. (eds.): Proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS’16), Lecture Notes in Computer Science, vol. 9933, Springer (2016)

  33. Vesely, W., Dugan, J., Fragola, J., Minarick, J., Railsback, J.: Fault Tree Handbook with Aerospace Applications. Tech. rep, NASA (2002)

  34. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Software & Systems Engineering, University of Augsburg, Augsburg, Germany

    Johannes Leupolz, Alexander Knapp, Axel Habermaier & Wolfgang Reif

Authors
  1. Johannes Leupolz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Knapp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Axel Habermaier
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Wolfgang Reif
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Johannes Leupolz.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Leupolz, J., Knapp, A., Habermaier, A. et al. Qualitative and quantitative analysis of safety-critical systems with . Int J Softw Tools Technol Transfer 20, 359–377 (2018). https://doi.org/10.1007/s10009-017-0464-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0464-3

Keywords

Search

Navigation