Skip to main content
SpringerLink
Log in

Monitoring Cyber-Physical Systems: From Design to Integration

  • Conference paper
  • First Online:
Runtime Verification (RV 2020)

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

Included in the following conference series:

Abstract

Cyber-physical systems are inherently safety-critical. The deployment of a runtime monitor significantly increases confidence in their safety. The effectiveness of the monitor can be maximized by considering it an integral component during its development. Thus, in this paper, I given an overview over recent work regarding a development process for runtime monitors alongside a cyber-physical system. This process includes the transformation of desirable safety properties into the formal specification language RTLola. A compiler then generates an executable artifact for monitoring the specification. This artifact can then be integrated into the system.

This work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (No. 683300).

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

Similar content being viewed by others

Notes

  1. 1.

    As a result, RTLola does not allow for accessing future values.

  2. 2.

    The hardware realization might require temporary registers and working memory. This can slightly increase the computed memory consumption.

  3. 3.

    https://www.xilinx.com/products/design-tools/vivado.html.

  4. 4.

    https://www.rust-lang.org/.

  5. 5.

    https://llvm.org/.

  6. 6.

    “Who will guard the guards themselves?”.

References

  1. Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3(OOPSLA), 147:1–147:30 (2019). https://doi.org/10.1145/3360573

    Article  Google Scholar 

  2. Basin, D., et al.: A formally verified, optimized monitor for metric first-order dynamic logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 432–453. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51074-9_25

    Chapter  Google Scholar 

  3. Basin, D.A., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015). https://doi.org/10.1145/2699444

    Article  MathSciNet  MATH  Google Scholar 

  4. Basin, D.A., Krstic, S., Traytel, D.: AERIAL: almost event-rate independent algorithms for monitoring metric regular properties. RV-CuBES 2017, 29–36 (2017)

    Google Scholar 

  5. Baumeister: Tracing Correctness: a practical Approach to Traceable Runtime Monitoring. Master thesis, Saarland University (2020)

    Google Scholar 

  6. Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28–39. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_3

    Chapter  Google Scholar 

  7. Baumeister, J., Finkbeiner, B., Schwenger, M., Torfah, H.: FPGA stream-monitoring of real-time properties. ACM Trans. Embedded Comput. Syst. 18(5s), 88:1–88:24 (2019). https://doi.org/10.1145/3358220

    Article  Google Scholar 

  8. Bourke, T., Brun, L., Dagand, P., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. In: Cohen, A., Vechev, M.T. (eds.) PLDI 2017, pp. 586–601. ACM (2017). https://doi.org/10.1145/3062341.3062358

  9. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15

    Chapter  MATH  Google Scholar 

  10. D’Angelo, B., et al.: Lola: runtime monitoring of synchronous systems. In: TIME 2005, pp. 166–174. IEEE Computer Society Press, June 2005

    Google Scholar 

  11. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. 51(1), 5–30 (2017). https://doi.org/10.1007/s10703-017-0286-7

    Article  MATH  Google Scholar 

  12. Drusinsky, D.: The temporal rover and the ATG rover. In: SPIN Model Checking and Software Verification, pp. 323–330 (2000). https://doi.org/10.1007/10722468_19

  13. Faymonville, P., et al.: StreamLAB: stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421–431. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_24

    Chapter  Google Scholar 

  14. Faymonville, P., Finkbeiner, B., Schwenger, M., Torfah, H.: Real-time Stream-based Monitoring. CoRR abs/1711.03829 (2017). http://arxiv.org/abs/1711.03829

  15. Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for lola specifications. In: RV 2020. LNCS. Springer (2020)

    Google Scholar 

  16. Finkbeiner, B., Schmidt, J., Schwenger, M.: Simplex architecture meets RTLola. In: MT@CPSWeek 2020 (2020). https://www.react.uni-saarland.de/publications/FSS20.pdf

  17. Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods Syst. Des. 24(2), 101–127 (2004). https://doi.org/10.1023/B:FORM.0000017718.28096.48

    Article  MATH  Google Scholar 

  18. Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. TACAS 2002, 342–356 (2002). https://doi.org/10.1007/3-540-46002-0_24

    Article  MATH  Google Scholar 

  19. Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Nickovic, D.: From signal temporal logic to FPGA monitors. MEMOCODE 2015, 218–227 (2015). https://doi.org/10.1109/MEMCOD.2015.7340489

    Article  Google Scholar 

  20. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/BF01995674

    Article  Google Scholar 

  21. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001). https://doi.org/10.1023/A:1011254632723

    Article  MATH  Google Scholar 

  22. Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. PDPTA 1999, 279–287 (1999)

    Google Scholar 

  23. Li, J., Maier, D., Tufte, K., Papadimos, V., Tucker, P.A.: No pane, no gain: efficient evaluation of sliding-window aggregates over data streams. SIGMOD Rec. 34(1), 39–44 (2005). https://doi.org/10.1145/1058150.1058158

    Article  Google Scholar 

  24. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: FORMATS 2004 and FTRTFT 2004, pp. 152–166 (2004). https://doi.org/10.1007/978-3-540-30206-3_12

  25. Meertens, L.: Algorithmics: towards programming as a mathematical activity (1986)

    Google Scholar 

  26. Mitsch, S., Platzer, A.: Modelplex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1–2), 33–74 (2016). https://doi.org/10.1007/s10703-016-0241-z

    Article  MATH  Google Scholar 

  27. Moosbrugger, P., Rozier, K.Y., Schumann, J.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods Syst. Des. 51(1), 31–61 (2017). https://doi.org/10.1007/s10703-017-0275-x

    Article  Google Scholar 

  28. Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2

    Chapter  MATH  Google Scholar 

  29. Nickovic, D., Maler, O.: AMT: A property-based monitoring tool for analog systems. FORMATS 2007, 304–319 (2007). https://doi.org/10.1007/978-3-540-75454-1_22

    Article  Google Scholar 

  30. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 345–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_26

    Chapter  Google Scholar 

  31. Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. ISSE 9(4), 235–255 (2013). https://doi.org/10.1007/s11334-013-0223-x

    Article  Google Scholar 

  32. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8

    Article  MathSciNet  MATH  Google Scholar 

  33. Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32

  34. Schneider, J., Basin, D., Krstić, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 310–328. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_18

    Chapter  Google Scholar 

  35. Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233–249. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_15

    Chapter  Google Scholar 

  36. Schwenger, M.: Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS. Master thesis, Saarland University (2019)

    Google Scholar 

  37. Sha, L.: Using simplicity to control complexity. IEEE Softw. 18(4), 20–28 (2001). https://doi.org/10.1109/MS.2001.936213

    Article  Google Scholar 

Download references

Acknowledgements

This paper is based on a tutorial at the 20th International Conference on Runtime Verification. The work summarized in this paper is based on several earlier publications  [6, 7, 13,14,15] and I am grateful to all my co-authors. I especially would also like to thank Jan Baumeister and Bernd Finkbeiner for providing valuable feedback and comments.

Author information

Authors and Affiliations

  1. CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

    Maximilian Schwenger

Authors
  1. Maximilian Schwenger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maximilian Schwenger .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Jyotirmoy Deshmukh

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

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

Schwenger, M. (2020). Monitoring Cyber-Physical Systems: From Design to Integration. In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-60508-7_5

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-030-60508-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation