Skip to main content
SpringerLink
Log in

Enforcing Timeliness and Safety in Mission-Critical Systems

  • Conference paper
  • First Online:
Reliable Software Technologies – Ada-Europe 2017 (Ada-Europe 2017)

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

Included in the following conference series:

  • 560 Accesses

Abstract

Advances in sensor, microprocessor and communication technologies have been fostering new applications of cyber-physical systems, often involving complex interactions between distributed autonomous components and the operation in harsh or uncertain contexts. This has led to new concerns regarding performance, safety and security, while ensuring timeliness requirements are met. To conciliate uncertainty with the required predictability, hybrid system architectures have been proposed, which separate the system in two parts: one that behaves in a best-effort way, depending on the context, and another that behaves as predictably as needed, providing critical services for a safe and secure operation. In this paper we address the problem of verifying the correct provisioning of critical functions at runtime in such hybrid architectures. We consider, in particular, the KARYON hybrid architecture and its Safety Kernel. We also consider a hardware-based non-intrusive runtime verification approach, describing how it is applied to verify Safety Kernel software functions. Finally, we experimentally evaluate the performance of two distinct Safety Kernel implementations and discuss the feasibility issues to incorporate non-intrusive runtime verification.

This work was partially supported by FCT, through funding of LaSIGE Research Unit, ref. UID/CEC/00408/2013. This work integrates the activities of COST Action IC1402 - Runtime Verification beyond Monitoring (ARVI), supported by COST (European Cooperation in Science and Technology).

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 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.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.

    A unit corresponds to a Safety Kernel information structure, concerning input (collected data), output (adjustment data) or locally calculated values. The term unit is coined from the Safety Kernel XML configuration file (Sect.3).

  2. 2.

    Most probably, there will be little to do anyway, if the design violation happens during a mission critical phase, such as the landing of a planetary probe. However, that does not necessarily imply the failure of the mission. For example: multiple (overload) alarms, occurring during the descendent flight of the first Moon landing, were advisedly discarded by the Apollo 11 lander crew.

  3. 3.

    This corresponds to the prefixes for binary multiples defined in the IEC 60027-2 standard specification [10].

References

  1. Aeroflex Gaisler, A.B., Goteborg, Sweden: GRLIB IP Library User’s Manual, April 2014

    Google Scholar 

  2. Antsaklis, P.J., Stiver, J.A., Lemmon, M.: Hybrid system modeling and autonomous control systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991–1992. LNCS, vol. 736, pp. 366–392. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_37

    Chapter  Google Scholar 

  3. ARM: ARM CoreSight Architecture Specification, 2.0 edn., September 2013

    Google Scholar 

  4. Backasch, R., Hochberger, C., Weiss, A., Leucker, M., Lasslop, R.: Runtime verification for multicore SoC with high-quality trace data. ACM Trans. Design Autom. Electron. Syst. (TODAES) 18(2), 18 (2013)

    Google Scholar 

  5. Callow, G., Watson, G., Kalawsky, R.: System modelling for run-time verification and validation of autonomous systems. In: Proceeding of 5th International Conference on System of Systems Engineering, Loughborough, UK, pp. 1–7, June 2010

    Google Scholar 

  6. Casimiro, A., Kaiser, J., Schiller, E.M., Costa, P., Parizi, J., Johansson, R., Librino, R.: The KARYON project: predictable and safe coordination in cooperative vehicular systems. In: Proceeding of 43rd Annual IEEE/IFIP Conference on Dependable Systems and Networks Workshop (DSN-W), pp. 1–12. IEEE (2013)

    Google Scholar 

  7. Casimiro, A., Rufino, J., Pinto, R.C., Vial, E., Schiller, E.M., Morales-Ponce, O., Petig, T.: A kernel-based architecture for safe cooperative vehicular functions. In: Proceeding of 9th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 228–237, June 2014

    Google Scholar 

  8. Correia, M., Veríssimo, P., Neves, N.F.: The design of a COTS real-time distributed security kernel. In: Bondavalli, A., Thevenod-Fosse, P. (eds.) EDCC 2002. LNCS, vol. 2485, pp. 234–252. Springer, Heidelberg (2002). doi:10.1007/3-540-36080-8_21

    Chapter  Google Scholar 

  9. Cotard, S., Faucou, S., Bechennec, J.L., Queudet, A., Trinquet, Y.: A data flow monitoring service based on runtime verification for AUTOSAR. In: Proceeding of 14th International Conference on High Performance Computing and Communications. IEEE, Liverpool, UK, June 2012

    Google Scholar 

  10. IEC Standards: IEC 60027-2: Letter symbols to be used in electrical technology Part 2: telecommunications and electronics, August 2005

    Google Scholar 

  11. Kane, A.: Runtime monitoring for safety-critical embedded systems. Ph.D. thesis, Carnegie Mellon University, USA, February 2015

    Google Scholar 

  12. Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Proceeding of 15th International Conference on Runtime Verification, Vienna, Austria, pp. 102–117, September 2015

    Google Scholar 

  13. Lee, J.C., Lysecky, R.: System-level observation framework for non-intrusive runtime monitoring of embedded systems. ACM Trans. Design Autom. Electron. Syst. 20, 42 (2015)

    Article  Google Scholar 

  14. Obermaisser, R., Kopetz, H.: Genesys: A candidate for an ARTEMIS cross-domain reference architecture for embedded systems, September 2009

    Google Scholar 

  15. On-Line Applications Research Corporation: RTEMS C User’s Guide, 4.9.4 edn. (2010)

    Google Scholar 

  16. Pinto, R.C., Rufino, J.: Towards non-invasive run-time verification of real-time systems. In: Proceeding of 26th Euromicro Conference on Real-Time Systems - WIP Session, Madrid, Spain, pp. 25–28, July 2014

    Google Scholar 

  17. Reinbacher, T., Fugger, M., Brauer, J.: Runtime verification of embedded real-time systems. Formal Methods Syst. Design 24(3), 203–239 (2014)

    Article  MATH  Google Scholar 

  18. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357–372. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_24

    Chapter  Google Scholar 

  19. Rufino, J., Gouveia, I.: Timeliness runtime verification and adaptation in avionic systems. In: Proceeding of 12th workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT), Toulouse, France, July 2016

    Google Scholar 

  20. Rufino, J.: Towards integration of adaptability and non-intrusive runtime verification in avionic systems. SIGBED Rev. 13(1), 60–65 (2016). (Special Issue on 5th Embedded Operating Systems Workshop)

    Article  Google Scholar 

  21. Sha, L.: Using simplicity to control complexity. IEEE Software 18(4), 20–28 (2001)

    Article  Google Scholar 

  22. Upton, E., Halfacree, G.: Raspberry Pi User Guide. Wiley, New York (2012)

    Google Scholar 

  23. Veríssimo, P.: Uncertainty and predictability: can they be reconciled? In: Schiper, A., Shvartsman, A.A., Weatherspoon, H., Zhao, B.Y. (eds.) Future Directions in DC 2002. LNCS, vol. 2584, pp. 108–113. Springer, Heidelberg (2003). doi:10.1007/3-540-37795-6_20

    Chapter  Google Scholar 

  24. Verissimo, P.: Travelling through wormholes: a new look at distributed systems models. SIGACT News 37(1), 66–81 (2006)

    Article  Google Scholar 

  25. Verissimo, P., Casimiro, A.: The timely computing base model and architecture. IEEE Trans. Comput. 51(8), 916–930 (2002)

    Article  Google Scholar 

  26. Vial, E., Casimiro, A.: Evaluation of safety rules in a safety kernel-based architecture. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 27–35. Springer, Cham (2014). doi:10.1007/978-3-319-10557-4_5

    Google Scholar 

  27. Watterson, C., Heffernan, D.: Runtime verification and monitoring of embedded systems. IET Software 1(5), 172–179 (2007)

    Article  Google Scholar 

  28. Zheng, X., Julien, C., Podorozhny, R., Cassez, F.: BraceAssertion: runtime verification of cyber-physical systems. In: Proceeding of 15th IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 298–306, October 2015

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LaSIGE, Faculdade de Ciências, Universidade de Lisboa, Lisbon, Portugal

    António Casimiro, Inês Gouveia & José Rufino

Authors
  1. António Casimiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Inês Gouveia
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José Rufino
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to António Casimiro .

Editor information

Editors and Affiliations

  1. Institute of Computer Aided Automation, Vienna University of Technology , Vienna, Austria

    Johann Blieberger

  2. Institute of Computer Aided Institute, Vienna University of Technology, Vienna, Austria

    Markus Bader

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Casimiro, A., Gouveia, I., Rufino, J. (2017). Enforcing Timeliness and Safety in Mission-Critical Systems. In: Blieberger, J., Bader, M. (eds) Reliable Software Technologies – Ada-Europe 2017. Ada-Europe 2017. Lecture Notes in Computer Science(), vol 10300. Springer, Cham. https://doi.org/10.1007/978-3-319-60588-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-60588-3_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-60587-6

  • Online ISBN: 978-3-319-60588-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation