iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-030-61470-6_25
Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification | SpringerLink
Skip to main content
Springer Nature Link
Log in

Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020)

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

Included in the following conference series:

Abstract

Future cyber-physical systems are expected to be dynamic, evolving while already being deployed. Frequent updates of software components are likely to become the norm even for safety-critical systems. In this setting, a full re-certification before each software update might delay important updates that fix previous bugs, or security or safety issues. Here we propose a vision addressing this challenge, namely through the evidence-based continuous supervision and certification of software variants in the field. The idea is to run both old and new variants of component software inside the same system, together with a supervising instance that monitors their behavior. Updated variants are phased into operation after sufficient evidence for correct behavior has been collected. The variants are required to explicate their decisions in a logical language, enabling the supervisor to reason about these decisions and to identify inconsistencies. To resolve contradictory information, the supervisor can run a component analysis to identify potentially faulty components on the basis of previously observed behavior, and can trigger micro-experiments which plan and execute system behavior specifically aimed at reducing uncertainty. We spell out our overall vision, and provide a first formalization of the different components and their interplay. In order to provide efficient supervisor reasoning as well as automatic verification of supervisor properties we introduce SupERLog, a logic specifically designed to this end.

Authors are listed alphabetically. This work was partially supported by the ERC Advanced Investigators Grant 695614 (POWVER), by DFG Grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science), and by the Key-Area Research and Development Program Grant 2018B010107004 of Guangdong Province.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

Notes

  1. 1.

    The idea is not limited to software components but expands to hardware components as well.

  2. 2.

    Note that, for the sake of efficiency, SupERLog reasoning may not explicitly handle negation. Instead, the relevant contradictory fact combinations can be identified via appropriate extra rules.

References

  1. Aizpurua, J., Muxika, E., Papadopoulos, Y., Chiacchio, F., Manno, G.: Application of the D3H2 methodology for the cost-effective design of dependable systems. Safety 2(2), 9 (2016). https://doi.org/10.3390/safety2020009

    Article  Google Scholar 

  2. Alur, R., Fisman, D., Raghothaman, M.: Regular programming for quantitative properties of data streams. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 15–40. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_2

    Chapter  MATH  Google Scholar 

  3. Alvaro, A., de Almeida, E.S., de Lemos Meira, S.R.: Software component certification: a survey. In: 31st EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 106–113 (2005)

    Google Scholar 

  4. Araya, M., Buffet, O., Thomas, V., Charpillet, F.: A POMDP extension with belief-dependent rewards. In: Lafferty, J.D., Williams, C.K.I., Shawe-Taylor, J., Zemel, R.S., Culotta, A. (eds.) Advances in Neural Information Processing Systems 23, pp. 64–72. Curran Associates, Inc. (2010)

    Google Scholar 

  5. Arnautov, S., Trach, B., Gregor, F., Knauth, T., Martin, A., Priebe, C., Lind, J., Muthukumaran, D., O’Keeffe, D., Stillwell, M.L., Goltzsche, D., Eyers, D., Kapitza, R., Pietzuch, P., Fetzer, C.: SCONE: secure Linux containers with intel SGX. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2016), Savannah, GA, pp. 689–703. USENIX Association (2016). https://www.usenix.org/conference/osdi16/technical-sessions/presentation/arnautov

  6. Avizienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput. 1(1), 11–33 (2004). https://doi.org/10.1109/TDSC.2004.2

    Article  Google Scholar 

  7. Avizienis, A., Laprie, J.C., Randell, B., et al.: Fundamental concepts of dependability. University of Newcastle upon Tyne, Computing Science (2001)

    Google Scholar 

  8. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_25

    Chapter  MATH  Google Scholar 

  9. Bishop, P., Bloomfield, R.: A methodology for safety case development, February 1998. https://doi.org/10.1007/978-1-4471-1534-2_14

  10. Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2010)

    MATH  Google Scholar 

  11. Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146–166 (1989)

    Article  Google Scholar 

  12. Council, N.R.: Software for Dependable Systems: Sufficient Evidence? The National Academies Press, Washington, DC (2007). https://doi.org/10.17226/11923. https://www.nap.edu/catalog/11923/software-for-dependable-systems-sufficient-evidence

  13. Currit, P.A., Dyer, M., Mills, H.D.: Certifying the reliability of software. IEEE Trans. Softw. Eng. SE–12(1), 3–11 (1986)

    Article  Google Scholar 

  14. D’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174 (2005)

    Google Scholar 

  15. Felser, M., Kapitza, R., Kleinöder, J., Schröder-Preikschat, W.: Dynamic software update of resource-constrained distributed embedded systems. In: Rettberg, A., Zanella, M.C., Dömer, R., Gerstlauer, A., Rammig, F.J. (eds.) IESS 2007. ITIFIP, vol. 231, pp. 387–400. Springer, Boston, MA (2007). https://doi.org/10.1007/978-0-387-72258-0_33

    Chapter  Google Scholar 

  16. Fiori, A., Weidenbach, C.: SCL with theory constraints. CoRR abs/2003.04627 (2020). https://arxiv.org/abs/2003.04627

  17. Fleury, M.: Formalization of logical calculi in Isabelle/HOL. Ph.D. thesis, Saarland University, Saarbrücken, Germany (2020)

    Google Scholar 

  18. Ghallab, M., Nau, D., Traverso, P.: Automated Planning and Acting. Cambridge University Press, Cambridge (2016)

    MATH  Google Scholar 

  19. Giro, S., D’Argenio, P.R., Fioriti, L.M.F.: Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms. Theoret. Comput. Sci. 538, 84–102 (2014). Quantitative Aspects of Programming Languages and Systems (2011–2012). https://doi.org/10.1016/j.tcs.2013.07.017. http://www.sciencedirect.com/science/article/pii/S0304397513005203

  20. Heck, H., Rudolph, S., Gruhl, C., Wacker, A., Hähner, J., Sick, B., Tomforde, S.: Towards autonomous self-tests at runtime. In: 2016 IEEE 1st International Workshops on Foundations and Applications of Self* Systems (FAS*W), pp. 98–99 (2016)

    Google Scholar 

  21. Heimerdinger, W., Weinstock, C.: A conceptual framework for system fault tolerance. Technical report CMU/SEI-92-TR-033, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (1992). http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11747

  22. Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays–Schönfinkel–Ramsey fragment with simple linear integer arithmetic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 77–94. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_6

    Chapter  Google Scholar 

  23. Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of Presburger arithmetic with unary uninterpreted predicates is undecidable. CoRR abs/1703.01212 (2017)

    Google Scholar 

  24. Kessler, A.M.: Elon musk says self-driving tesla cars will be in the US by summer. The New York Times 19, 1 (2015). https://www.nytimes.com/2015/03/20/business/elon-musk-says-self-driving-tesla-cars-will-be-in-the-us-by-summer.html

  25. Kuvaiskii, D., Faqeh, R., Bhatotia, P., Felber, P., Fetzer, C.: HAFT: hardware-assisted fault tolerance. In: Proceedings of the Eleventh European Conference on Computer Systems, EuroSys 2016. Association for Computing Machinery, New York (2016). https://doi.org/10.1145/2901318.2901339

  26. Kuvaiskii, D., Fetzer, C.: \(\delta \)-encoding: Practical encoded processing (2015)

    Google Scholar 

  27. Kuvaiskii, D., Oleksenko, O., Arnautov, S., Trach, B., Bhatotia, P., Felber, P., Fetzer, C.: SGXBOUNDS: memory safety for shielded execution. In: Proceedings of the Twelfth European Conference on Computer Systems, EuroSys 2017, pp. 205–221. Association for Computing Machinery, New York (2017). https://doi.org/10.1145/3064176.3064192

  28. Kuvaiskii, D., Oleksenko, O., Bhatotia, P., Felber, P., Fetzer, C.: ELZAR: triple modular redundancy using intel AVX (practical experience report). In: 2016 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), June 2016. https://doi.org/10.1109/dsn.2016.65

  29. Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513–532 (2020)

    Article  MathSciNet  Google Scholar 

  30. Laprie, J.C.: Dependability: basic concepts and terminology. In: Laprie, J.C. (ed.) Dependability: Basic Concepts and Terminology. DEPENDABLECOMP, vol. 5, pp. 3–245. Springer, Vienna (1992). https://doi.org/10.1007/978-3-7091-9170-5_1

    Chapter  MATH  Google Scholar 

  31. Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Schramm, A.: TeSSLa: runtime verification of non-synchronized real-time streams. In: ACM Symposium on Applied Computing (SAC), France. ACM, April 2018

    Google Scholar 

  32. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293–303 (2009). The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS ’07)

    Article  Google Scholar 

  33. Lynch, N.: Input/output automata: basic, timed, hybrid, probabilistic, dynamic, In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 191–192. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45187-7_12

    Chapter  Google Scholar 

  34. Lyyra, A.K., Koskinen, K.M.: With software updates, Tesla upends product life cycle in the car industry. LSE Bus. Rev. (2017)

    Google Scholar 

  35. Moore, E.F., et al.: Gedanken-experiments on sequential machines. Automata Stud. 34, 129–153 (1956)

    MathSciNet  Google Scholar 

  36. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 937–977 (2006)

    Article  MathSciNet  Google Scholar 

  37. Palin, R., Ward, D., Habli, I., Rivett, R.: ISO 26262 safety cases: Compliance and assurance, vol. 2011, September 2011. https://doi.org/10.1049/cp.2011.0251

  38. Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes, 25, 206–230 (1987). https://doi.org/10.1007/BFb0006306

  39. Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 3rd edn. Prentice Hall, Upper Saddle River (2010)

    MATH  Google Scholar 

  40. Salfner, F., Malek, M.: Architecting dependable systems with proactive fault management. In: Casimiro, A., de Lemos, R., Gacek, C. (eds.) WADS 2009. LNCS, vol. 6420, pp. 171–200. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17245-8_8

    Chapter  Google Scholar 

  41. Saltzer, J.H., Reed, D.P., Clark, D.D.: End-to-end arguments in system design. ACM Trans. Comput. Syst. 2(4), 277–88 (1984). https://doi.org/10.1145/357401.357402

    Article  Google Scholar 

  42. Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv. (CSUR) 22(4), 299–319 (1990)

    Article  Google Scholar 

  43. Voigt, M.: The Bernays–Schönfinkel–Ramsey fragment with bounded difference constraints over the reals is decidable. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 244–261. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_14

    Chapter  Google Scholar 

  44. Wu, W., Kelly, T.: Safety tactics for software architecture design. In: Proceedings of the 28th Annual International Computer Software and Applications Conference 2004, COMPSAC 2004, vol. 1, pp. 368–375 (2004)

    Google Scholar 

  45. Åström, K.: Optimal control of Markov processes with incomplete state information. J. Math. Anal. Appl. 10(1), 174–205 (1965). https://doi.org/10.1016/0022-247X(65)90154-X

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Dresden, Dresden, Germany

    Rasha Faqeh & Christof Fetzer

  2. Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

    Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Maximilian A. Köhl & Marcel Steinmetz

  3. Institute of Intelligent Software, Guangzhou, China

    Holger Hermanns

  4. Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

    Christoph Weidenbach

Authors
  1. Rasha Faqeh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christof Fetzer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jörg Hoffmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Michaela Klauck
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Maximilian A. Köhl
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Marcel Steinmetz
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Christoph Weidenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Rasha Faqeh , Christof Fetzer , Holger Hermanns , Jörg Hoffmann , Michaela Klauck , Maximilian A. Köhl , Marcel Steinmetz or Christoph Weidenbach .

Editor information

Editors and Affiliations

  1. University of Limerick and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Faqeh, R. et al. (2020). Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12477. Springer, Cham. https://doi.org/10.1007/978-3-030-61470-6_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61470-6_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61469-0

  • Online ISBN: 978-3-030-61470-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation