Skip to main content
SpringerLink
Log in

A Contracts-Based Framework for Systems Modeling and Embedded Diagnostics

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

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

Included in the following conference series:

Abstract

Two key impediments for the commercial success of model-based diagnosis (MBD) include (a) a failure to integrate diagnostics modeling within the requirements and design phase, and (b) a high degree of diagnostic ambiguity during run-time. This article addresses both of these impediments by providing a formal framework that integrates requirements-based design with MBD modeling. The proposed framework extends the consistency-based theory of MBD with a requirements-based design theory based on contracts.

Gregory Provan—Supported by SFI grant 12/RC/1189.

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

Notes

  1. 1.

    Note that we suppress temporal indexing to simplify the notation.

  2. 2.

    The proof is provided in the supplementary material.

References

  1. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Chilton, C., Jonsson, B., Kwiatkowska, M.: Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program. 91, 115–137 (2014)

    Article  Google Scholar 

  3. Debouk, R., Lafortune, S., Teneketzis, D.: Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discrete Event Dyn. Syst. 10(1–2), 33–86 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Giese, H., Henkler, S., Hirsch, M.: A multi-paradigm approach supporting the modular execution of reconfigurable hybrid systems. In: Transactions of the Society for Modeling and Simulation International (2010)

    Google Scholar 

  5. Hashtrudi Zad, S., Kwong, R., Wonham, W.: Fault diagnosis in timed discrete-event systems. In: Proceedings of the 38th IEEE Conference on Decision and Control, vol. 2, pp. 1756–1761. IEEE (1999)

    Google Scholar 

  6. Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans. Autom. Control 46(8), 1318–1321 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. Jiang, S., Kumar, R.: Failure diagnosis of discrete-event systems with linear-time temporal logic specifications. IEEE Trans. Autom. Control 49(6), 934–945 (2004)

    Article  MathSciNet  Google Scholar 

  8. Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  9. Martin, A., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15, 73–132 (1993)

    Article  Google Scholar 

  10. Meyer, B., Fiva, A., Ciupa, I., Leitner, A., Wei, Y., Stapf, E.: Programs that test themselves. Computer 42(9), 46–55 (2009)

    Article  Google Scholar 

  11. Pill, I., Quaritsch, T.: An ltl sat encoding for behavioral diagnosis. In: International Workshop on the Principles of Diagnosis, pp. 67–74 (2012)

    Google Scholar 

  12. Pill, I., Quaritsch, T.: Behavioral diagnosis of ltl specifications at operator level. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, pp. 1053–1059. AAAI Press (2013)

    Google Scholar 

  13. Prokhorova, Y., Troubitsyna, E.: A survey of safety-oriented model-driven and formal development approaches. Int. J. Crit. Comput.-Based Syst. 4(2), 93–118 (2013)

    Article  Google Scholar 

  14. Quaritsch, T., Pill, I.: Pymbd: A library of mbd algorithms and a light-weight evaluation platform. In: Proceedings of Dx-2014 (2014)

    Google Scholar 

  15. Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae 108(1), 119–149 (2011)

    MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  17. Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.C.: Failure diagnosis using discrete-event models. IEEE Trans. Control Syst. Technol. 4(2), 105–124 (1996)

    Article  Google Scholar 

  18. Slâtten, V.: Model-Driven Engineering of Dependable Systems. In: 2010 Third International Conference on Software Testing, Verification and Validation, pp. 359–362. IEEE (2010)

    Google Scholar 

  19. Stirling, C.: Modal and temporal logics (1991)

    Google Scholar 

  20. Sun, X., Nuzzo, P., Wu, C., Sangiovanni-Vincentelli, A.: Contract-based system-level composition of analog circuits. In: Proceedings of the 46th Annual Design Automation Conference, pp. 605–610. ACM (2009)

    Google Scholar 

  21. Zulkernine, M., Seviora, R.: Towards automatic monitoring of component-based software systems. J. Syst. Softw. 74(1), 15–24 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University College Cork, Cork, Ireland

    Gregory Provan

Authors
  1. Gregory Provan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gregory Provan .

Editor information

Editors and Affiliations

  1. University of Malaga, Malaga, Spain

    Carlos Canal

  2. LIG Lab, Saint Martin d'Hères Cedex, France

    Akram Idani

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Provan, G. (2015). A Contracts-Based Framework for Systems Modeling and Embedded Diagnostics. In: Canal, C., Idani, A. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science(), vol 8938. Springer, Cham. https://doi.org/10.1007/978-3-319-15201-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15201-1_9

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation