Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis

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


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 Open image in new window (“safety sharp”).


Model Check Fault Activation Linear Temporal Logic Reachable State Fault Injection 
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.


  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.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  4. 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. 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)CrossRefGoogle Scholar
  6. 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)CrossRefGoogle Scholar
  7. 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)CrossRefGoogle Scholar
  8. 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)CrossRefGoogle Scholar
  9. 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)CrossRefGoogle Scholar
  10. 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)CrossRefGoogle Scholar
  11. 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)CrossRefGoogle Scholar
  12. 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. 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. 14.
    Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2004)Google Scholar
  15. 15.
    ISO: ISO/IEC 23270: Information technology - Programming languages – C# (2006)Google Scholar
  16. 16.
    ISO: ISO/IEC 23271: Information technology – Common Language Infrastructure (2012)Google Scholar
  17. 17.
    ISO/IEC/IEEE: ISO 24765: Systems and software engineering – Vocabulary (2010)Google Scholar
  18. 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. 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. 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. 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. 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 CrossRefGoogle Scholar
  23. 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. 24.
    Object Management Group: OMG Systems Modeling Language (OMG SysML), Version 1.4 (2015)Google Scholar
  25. 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)CrossRefGoogle Scholar
  26. 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)CrossRefGoogle Scholar
  27. 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. 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. 29.
    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
  • Alexander Knapp
    • 1
  • Johannes Leupolz
    • 1
  • Wolfgang Reif
    • 1
  1. 1.Institute for Software and Systems EngineeringUniversity of AugsburgAugsburgGermany

Personalised recommendations