Skip to main content
SpringerLink
Log in

A Diagnosis Framework for Critical Systems Verification (Short Paper)

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10469))

Included in the following conference series:

Abstract

For critical systems design, the verification tasks play a crucial role. If abnormalities are detected, a diagnostic process must be started to find and understand the root causes before corrective actions are applied. Detection and diagnosis are notions that overlap in common speech. Detection basically means to identify something as unusual, diagnosis means to investigate its root cause. The meaning of diagnosis is also fuzzy, because diagnosis is either an activity - an investigation - or an output result - the nature or the type of a problem. This paper proposes an organizational framework for structuring diagnoses around three principles: that propositional data (including detection) are the inputs of the diagnostic system; that activities are made of methods and techniques; and that associations specialize that relationships between the two preceding categories.

This is a short paper accepted in the new ideas and work-in-progress section of SEFM 2017.

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

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Dictionary—Merriam-Webster. https://www.merriam-webster.com

  2. Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: Automated support for iagnosis and repair. Commu. ACM 58(2), 65–72 (2015)

    Article  Google Scholar 

  3. Aviienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and axonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 1(1), 11–33 (2004)

    Article  Google Scholar 

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

    MATH  Google Scholar 

  5. Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: ACM SIGPLAN, vol. 38. ACM (2003)

    Article  Google Scholar 

  6. Bertoli, P., Bozzano, M., Cimatti, A.: A symbolic model checking framework for safety analysis, diagnosis, and synthesis. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS, vol. 4428, pp. 1–18. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74128-2_1

    Chapter  MATH  Google Scholar 

  7. Bourahla, M.: Model-based diagnostic using model checking. In: 2009 Fourth International Conference on Dependability of Computer Systems, Brunow, pp. 229–236 (2009). doi:10.1109/DepCoS-RELCOMEX.2009.33

  8. Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artif. Intell. 112(1), 57–104 (1999)

    Article  MathSciNet  Google Scholar 

  9. Cleve, H., Zeller, A.: Locating causes of program failures, p. 342. ACM Press (2005)

    Google Scholar 

  10. Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 121–136. Springer, Heidelberg (2003). doi:10.1007/3-540-44829-2_8

    Chapter  Google Scholar 

  11. Gromov, M., Willemse, T.A.C.: Testing and model-checking techniques for diagnosis. In: Petrenko, A., Veanes, M., Tretmans, J., Grieskamp, W. (eds.) FATES/TestCom -2007. LNCS, vol. 4581, pp. 138–154. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73066-8_10

    Chapter  Google Scholar 

  12. Hamou-Lhadj, A., Lethbridge, T.C.: A survey of trace exploration tools and techniques. In: CASCON 2004, pp. 42–55. IBM Press (2004)

    Google Scholar 

  13. Holzmann, G.J.: The theory and practice of a formal method: NewCoRe. In: IFIP Congress (1), pp. 35–44 (1994)

    Google Scholar 

  14. Leilde, V., Ribaud, V., Dhaussy, P.: An organizing system to perform and enable verification and diagnosis activities. In: Yin, H., Gao, Y., Li, B., Zhang, D., Yang, M., Li, Y., Klawonn, F., Tallón-Ballesteros, A.J. (eds.) IDEAL 2016. LNCS, vol. 9937, pp. 576–587. Springer, Cham (2016). doi:10.1007/978-3-319-46257-8_62

    Chapter  Google Scholar 

  15. Liu, Y., Xu, C., Cheung, S.: AFChecker: effective model checking for context-aware adaptive applications. J. Syst. Softw. 86(3), 854–867 (2013)

    Article  Google Scholar 

  16. Mackie, J.L.: The Cement of the Universe: A study of causation. Clarendon Library of Logic and Philosophy, 5. dr. edn. Clarendon Press, Oxford (1990). oCLC: 258760915

    Google Scholar 

  17. Pothier, G., Tanter, É., Piquer, J.: Scalable omniscient debugging. ACM SIGPLAN Not. 42(10), 535–552 (2007)

    Article  Google Scholar 

  18. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32, 57–95 (1987)

    Article  MathSciNet  Google Scholar 

  19. Ruys, T.C., Brinksma, E.: Managing the verification trajectory. Int. J. Softw. Tools Technol. Transf. (STTT) 4(2), 246–259 (2003)

    Article  Google Scholar 

  20. Venkatasubramanian, V., Rengaswamy, R., Kavuri, S.N.: A review of process fault detection and diagnosis. Comput. Chem. Eng. 27(3), 293–311 (2003)

    Article  Google Scholar 

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

    Article  Google Scholar 

  22. Wotawa, F., Rodriguez-Roda, I., Comas, J.: Abductive reasoning in environmental decision support systems. In: AIAI workshops, pp. 270–279. Citeseer (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lab-STICC, Team MOCS, ENSTA-Bretagne, rue Fran çois Verny, Brest, France

    Vincent Leildé, Ciprian Teodorov & Philippe Dhaussy

  2. Lab-STICC, Team MOCS, Université de Bretagne Occidentale, Avenue le Gorgeu, Brest, France

    Vincent Ribaud

Authors
  1. Vincent Leildé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vincent Ribaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ciprian Teodorov
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Philippe Dhaussy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vincent Leildé .

Editor information

Editors and Affiliations

  1. University of Trento, Trento, Italy

    Alessandro Cimatti

  2. Mälardalen University, Västerås, Sweden

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Leildé, V., Ribaud, V., Teodorov, C., Dhaussy, P. (2017). A Diagnosis Framework for Critical Systems Verification (Short Paper). In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66197-1_27

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation