Skip to main content
SpringerLink
Log in

Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis

  • Conference paper
  • First Online:
Book cover Critical Systems: Formal Methods and Automated Verification (AVoCS 2016, FMICS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9933))

Abstract

Deductive Cause Consequence Analysis (Dcca) is a model checking-based safety analysis technique that determines all combinations of faults potentially causing a hazard. This paper introduces a new fault modeling and specification approach for safety-critical systems based on the concept of fault activations that decreases explicit-state model checking and safety analysis times by up to three orders of magnitude. We augment Kripke structures and LTL with fault activations and show how standard model checkers can be used for analysis. Additionally, we present conceptual changes to Dcca that improve efficiency and usability. We evaluate our work using our safety analysis tool (“safety sharp”).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

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.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

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

    MATH  Google Scholar 

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

  5. Bozzano, M., Cimatti, A., Griggio, A., Mattarei, C.: Efficient anytime techniques for model-based safety analysis. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 603–621. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  6. Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173–186. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 162–176. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  9. Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1–26. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Grunske, L., Kaiser, B.: An automated dependability analysis method for COTS-based systems. In: Franch, X., Port, D. (eds.) ICCBSS 2005. LNCS, vol. 3412, pp. 178–190. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Güdemann, M., Ortmeier, F., Reif, W.: Using deductive cause-consequence analysis (DCCA) with SCADE. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 465–478. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

  13. Habermaier, A., Knapp, A., Leupolz, J., Reif, W.: Unified simulation, visualization, and formal analysis of safety-critical systems with S#. In: ter Beek, M., Gnesi, S., Knapp, A. (eds.) FMICS-AVoCS 2016. LNCS, vol. 9933, pp. 150–167. Springer, Heidelberg (2016)

    Google Scholar 

  14. Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2004)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  17. ISO/IEC/IEEE: ISO 24765: Systems and software engineering – Vocabulary (2010)

    Google Scholar 

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

  19. Kromodimoeljo, S., Lindsay, P.A.: Automatic Generation of Minimal Cut Sets. In: Engineering Safety and Security Systems, pp. 33–47 (2015)

    Google Scholar 

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

  21. Markey, N.: Temporal logic with past is exponentially more succinct. In: EATCS Bulletin, vol. 79, pp. 122–128. European Association for Theoretical Computer Science (2003)

    Google Scholar 

  22. Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33600-8_29

    Chapter  Google Scholar 

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

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

    Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Papadopoulos, Y., Walker, M., Parker, D., Rüde, E., Hamann, R., Uhlig, A., Grätz, U., Lien, R.: Engineering failure analysis and design optimisation with HiP-HOPS. Eng. Fail. Anal. 18(2), 590–608 (2011)

    Article  Google Scholar 

  27. Pradella, M., San Pietro, P., Spoletini, P., Morzenti, A.: Practical model checking of LTL with past. In: Automated Technology for Verification and Analysis (2003)

    Google Scholar 

  28. Vesely, W., Dugan, J., Fragola, J., Minarick, J., Railsback, J.: Fault tree handbook with aerospace applications. Technical report, NASA, Washington, DC (2002)

    Google Scholar 

  29. 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 and Systems Engineering, University of Augsburg, Augsburg, Germany

    Axel Habermaier, Alexander Knapp, Johannes Leupolz & Wolfgang Reif

Authors
  1. Axel Habermaier
    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. Johannes Leupolz
    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 Axel Habermaier .

Editor information

Editors and Affiliations

  1. ISTI-CNR , Pisa, Italy

    Maurice H. ter Beek

  2. ISTI-CNR , Pisa, Italy

    Stefania Gnesi

  3. Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Habermaier, A., Knapp, A., Leupolz, J., Reif, W. (2016). Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45943-1_7

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation