Advertisement

Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with Open image in new window

  • Axel HabermaierEmail author
  • Johannes Leupolz
  • Wolfgang Reif
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)

Abstract

We give an overview of the Open image in new window (pronounced “safety sharp”) framework for rigorous, model-based analysis of safety-critical systems. We introduce Open image in new window ’s expressive modeling language based on the Open image in new window programming language, showing how Open image in new window ’s fault modeling and flexible model composition capabilities can be used to model a case study from the transportation sector with multiple design variants. Fully automated formal safety analyses are conducted for the case study using the explicit-state model checker LTSmin. Analysis efficiency is evaluated in comparison with other safety analysis tools and model checkers.

Keywords

Kripke Structure Nondeterministic Choice Height Control Execution Semantic Left Lane 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 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.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Avižienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. Dependable Secure Comput. 1(1), 11–33 (2004)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Butcher, J.: The Numerical Analysis of Ordinary Differential Equations: Runge-Kutta and General Linear Methods, 2nd edn. Wiley, Hoboken (2003)CrossRefGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Habermaier, A., Eberhardinger, B., Seebach, H., Leupolz, J., Reif, W.: Runtime model-based safety analysis of self-organizing systems with S#. In: Self-Adaptive and Self-Organizing Systems Workshops, pp. 128–133 (2015)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Habermaier, A., Knapp, A., Leupolz, J., Reif, W.: Fault-aware modeling and specification for efficient formal safety analysis. In: ter Beek, M., Gnesi, S., Knapp, A. (eds.) FMICS-AVoCS 2016. LNCS, vol. 9933, pp. 97–114. Springer, Heidelberg (2016)Google Scholar
  9. 9.
    Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2004)Google Scholar
  10. 10.
    ISO: ISO/IEC 23270: Information technology– Programming languages–C# (2006)Google Scholar
  11. 11.
    ISO: ISO 24765: Systems and software engineering - Vocabulary (2010)Google Scholar
  12. 12.
    ISO: ISO/IEC 23271: Information technology - Common Language Infrastructure (2012)Google Scholar
  13. 13.
    Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Kirsch, C., Sengupta, R.: The evolution of real-time programming. In: Kirsch, C., Sengupta, R. (eds.) Handbook of Real-Time and Embedded Systems. CRC Press (2007)Google Scholar
  16. 16.
    Leveson, N.: Engineering a Safer World. MIT Press, Cambridge (2011)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Noll, T.: Safety, dependability and performance analysis of aerospace systems. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 17–31. Springer, Heidelberg (2015)Google Scholar
  19. 19.
    Object Management Group: OMG Systems Modeling Language, Version 1.4 (2015)Google Scholar
  20. 20.
    Ortmeier, F., Schellhorn, G., Thums, A., Reif, W., Hering, B., Trappschuh, H.: Safety analysis of the height control system for the Elbtunnel. In: Anderson, S., Bologna, S., Felici, M. (eds.) SAFECOMP 2002. LNCS, vol. 2434, pp. 296–308. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6: 1–6: 45 (2014)CrossRefGoogle Scholar
  22. 22.
    Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Axel Habermaier
    • 1
    Email author
  • Johannes Leupolz
    • 1
  • Wolfgang Reif
    • 1
  1. 1.Institute for Software and Systems EngineeringUniversity of AugsburgAugsburgGermany

Personalised recommendations