Enforcing Timeliness and Safety in Mission-Critical Systems

  • António CasimiroEmail author
  • Inês Gouveia
  • José Rufino
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10300)


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.


Real-time and embedded systems Software architectures Architecture hybridization Reliability and safety Runtime verification 


  1. 1.
    Aeroflex Gaisler, A.B., Goteborg, Sweden: GRLIB IP Library User’s Manual, April 2014Google Scholar
  2. 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 CrossRefGoogle Scholar
  3. 3.
    ARM: ARM CoreSight Architecture Specification, 2.0 edn., September 2013Google Scholar
  4. 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. 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 2010Google Scholar
  6. 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. 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 2014Google Scholar
  8. 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 CrossRefGoogle Scholar
  9. 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 2012Google Scholar
  10. 10.
    IEC Standards: IEC 60027-2: Letter symbols to be used in electrical technology Part 2: telecommunications and electronics, August 2005Google Scholar
  11. 11.
    Kane, A.: Runtime monitoring for safety-critical embedded systems. Ph.D. thesis, Carnegie Mellon University, USA, February 2015Google Scholar
  12. 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 2015Google Scholar
  13. 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)CrossRefGoogle Scholar
  14. 14.
    Obermaisser, R., Kopetz, H.: Genesys: A candidate for an ARTEMIS cross-domain reference architecture for embedded systems, September 2009Google Scholar
  15. 15.
    On-Line Applications Research Corporation: RTEMS C User’s Guide, 4.9.4 edn. (2010)Google Scholar
  16. 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 2014Google Scholar
  17. 17.
    Reinbacher, T., Fugger, M., Brauer, J.: Runtime verification of embedded real-time systems. Formal Methods Syst. Design 24(3), 203–239 (2014)CrossRefzbMATHGoogle Scholar
  18. 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 CrossRefGoogle Scholar
  19. 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 2016Google Scholar
  20. 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)CrossRefGoogle Scholar
  21. 21.
    Sha, L.: Using simplicity to control complexity. IEEE Software 18(4), 20–28 (2001)CrossRefGoogle Scholar
  22. 22.
    Upton, E., Halfacree, G.: Raspberry Pi User Guide. Wiley, New York (2012)Google Scholar
  23. 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 CrossRefGoogle Scholar
  24. 24.
    Verissimo, P.: Travelling through wormholes: a new look at distributed systems models. SIGACT News 37(1), 66–81 (2006)CrossRefGoogle Scholar
  25. 25.
    Verissimo, P., Casimiro, A.: The timely computing base model and architecture. IEEE Trans. Comput. 51(8), 916–930 (2002)CrossRefGoogle Scholar
  26. 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. 27.
    Watterson, C., Heffernan, D.: Runtime verification and monitoring of embedded systems. IET Software 1(5), 172–179 (2007)CrossRefGoogle Scholar
  28. 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 2015Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • António Casimiro
    • 1
    Email author
  • Inês Gouveia
    • 1
  • José Rufino
    • 1
  1. 1.LaSIGE, Faculdade de CiênciasUniversidade de LisboaLisbonPortugal

Personalised recommendations