Skip to main content
SpringerLink
Log in

Invariant Management in the Presence of Failures

  • Conference paper
  • First Online:
Book cover Model-Based Safety and Assessment (IMBSA 2017)

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

Included in the following conference series:

  • 835 Accesses

Abstract

In the effort to develop critical systems, taking account of failure modes is of vital importance. However, when systems fail (even in a manner previously determined as acceptable), a lot of the invariants that hold in the case of nominal behaviour also fail. A technique is proposed that permits the inclusion of the strong invariants of nominal behaviour alongside the provisions for degraded behaviour in an inclusive formal system model. The faulty system model is derived from the nominal one via fault injection, and the nominal and faulty system models are related via a formal retrenchment step. Manipulation of the retrenchment data permits the inclusion of the stronger invariants, which remain provable when faults are disabled in a generic manner in the faulty model, thus increasing confidence in the overall system design. The details are developed in Event-B, and the concept is illustrated using a toy switching example.

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.

    Of course, in reality, the fault portfolio is contemplated from the earliest stages of development, but we do not include any failure modes in the early stages of formal modelling.

  2. 2.

    The generalised kind of guard used in retrenchment is typically referred to as the WITHIN clause in work on retrenchment.

  3. 3.

    We write ‘non-refining’ in quotes because we have carefully defined the joint invariants to be oblivious to the faulty behaviour.

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  2. Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Soft. Tools Tech. Trans. 12(6), 447–466 (2010)

    Article  Google Scholar 

  3. ADVANCE: European Project ADVANCE. IST-287563. http://www.advance-ict.eu/

  4. Back, R.J.R., Sere, K.: Stepwise refinement of action systems. In: Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 115–138. Springer, Heidelberg (1989). doi:10.1007/3-540-51305-1_7

    Chapter  Google Scholar 

  5. Back, R.J.R., Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994). doi:10.1007/978-3-540-48654-1_28

    Chapter  Google Scholar 

  6. Back, R., Kurki-Suonio, R.: Decentralisation of process nets with centralised control. In: 2nd ACM SIGACT-SIGOPS Symposium on PODC, pp. 131–142. ACM (1983)

    Google Scholar 

  7. Back, R., Sere, K.: Superposition refinement of reactive systems. Form. Asp. Comp. 8(3), 324–346 (1996)

    Article  MATH  Google Scholar 

  8. Banach, R.: A deidealisation semantics for KAOS. In: Lencastre, M. (ed.) Proceedings of the ACM SAC 2010 (RE track), pp. 267–274. ACM (2010)

    Google Scholar 

  9. Banach, R., Bozzano, M.: The mechanical generation of fault trees for reactive systems via retrenchment I: combinational circuits. Form. Asp. Comp. 25, 573–607 (2013)

    Article  MATH  Google Scholar 

  10. Banach, R., Bozzano, M.: The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits. Form. Asp. Comp. 25, 609–657 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  11. Banach, R., Jeske, C.: Retrenchment and refinement interworking: the tower theorems. Math. Struct. Comput. Sci. 25, 135–202 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  12. Banach, R., Jeske, C., Poppleton, M.: Composition mechanisms for retrenchment. J. Log. Alg. Program. 75, 209–229 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  13. Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comput. Program. 67, 301–329 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007). doi:10.1007/978-3-540-69738-1_27

    Chapter  Google Scholar 

  15. Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 533–539. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_31

    Chapter  Google Scholar 

  16. Bozzano, M., Villafiorita, A.: Design and Safety Assessment of Critical Systems. CRC Press (Taylor and Francis), an Auerbach Book, Boca Raton (2010)

    Google Scholar 

  17. DEPLOY: European Project DEPLOY. IST-511599. http://www.deploy-project.eu/

  18. Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351–368. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23702-7_26

    Chapter  Google Scholar 

  19. Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 277–300. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15025-8_15

    Chapter  Google Scholar 

  20. Ghilardi, S., Ranise, S.: Goal-directed invariant synthesis for model checking modulo theories. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 173–188. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02716-1_14

    Chapter  Google Scholar 

  21. van Lamsweerde, A.: Requirements Engineering: From System Goals to UML Models to Software Specifications. Wiley, Chichester (2009)

    Google Scholar 

  22. Letier, E.: Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph.D. thesis, Dépt. Ingénierie Informatique, Université Catholique de Louvain (2001)

    Google Scholar 

  23. Qin, S., He, G., Luo, C., Chin, W.N.: Loop invariant synthesis in a combined domain. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 468–484. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16901-4_31

    Chapter  Google Scholar 

  24. RODIN: European Project RODIN (Rigorous Open Development for Complex Systems) IST-511599. http://rodin.cs.ncl.ac.uk/

  25. Sekerinski, E., Sere, K.: Program Development by Refinement: Case Studies Using the B-Method. Springer, London (1998)

    MATH  Google Scholar 

  26. Voisin, L., Abrial, J.R.: The rodin platform has turned ten. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8847, pp. 1–8. Springer, Heidelberg (2014). doi:10.1007/978-3-662-43652-3_1

    Google Scholar 

  27. Wahl, T.: The \(k\)-induction principle. http://www.ccs.neu.edu/home/wahl/Publications/k-induction.pdf

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Manchester, Oxford Road, Manchester, M13 9PL, UK

    Richard Banach

Authors
  1. Richard Banach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Richard Banach .

Editor information

Editors and Affiliations

  1. Fondazione Bruno Kessler, Trento, Italy

    Marco Bozzano

  2. University of Hull, Hull, United Kingdom

    Yiannis Papadopoulos

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Banach, R. (2017). Invariant Management in the Presence of Failures. In: Bozzano, M., Papadopoulos, Y. (eds) Model-Based Safety and Assessment. IMBSA 2017. Lecture Notes in Computer Science(), vol 10437. Springer, Cham. https://doi.org/10.1007/978-3-319-64119-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-64119-5_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-64118-8

  • Online ISBN: 978-3-319-64119-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation