Skip to main content
SpringerLink
Log in

MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties

  • 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

We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile and spatially distributed cyber-physical systems (CPS). In the proposed framework, space is represented as a weighted graph, describing the topological configurations in which the single CPS entities (nodes of the graph) are arranged. Both nodes and edges have attributes modelling physical and logical quantities that can change in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL) introduced in  [6]. MoonLight can be used as a standalone command line tool, as a Java API, or via Matlab ™interface. We provide here some examples using the Matlab ™interface and we evaluate the tool performance also by comparing with other tools specialized in monitoring only temporal properties.

This research has been partially supported by the Austrian FWF projects ZK-35 and W1255-N23, by the Italian PRIN project “SEDUCE” n. 2017TWRCNB and by the Italian PRIN project “IT-MaTTerS” n, 2017FTXR7S.

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

References

  1. Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: A survey on sensor networks. IEEE Commun. Mag. 40(8), 102–114 (2002). https://doi.org/10.1109/MCOM.2002.1024422

    Article  Google Scholar 

  2. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_21

    Chapter  MATH  Google Scholar 

  3. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002). https://doi.org/10.1145/506147.506151

    Article  MathSciNet  MATH  Google Scholar 

  4. Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_5

    Chapter  Google Scholar 

  5. Chockler, H., Weissenbacher, G. (eds.): CAV 2018. LNCS, vol. 10981. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3

    Book  MATH  Google Scholar 

  6. Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proc. of MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 146–155. ACM (2017) https://doi.org/10.1145/3127041.3127050

  7. Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1

    Chapter  Google Scholar 

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

  9. Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_17

    Chapter  Google Scholar 

  10. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009). https://doi.org/10.1016/j.tcs.2009.06.021

    Article  MathSciNet  MATH  Google Scholar 

  11. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proc. of HSCC’15: the 18th International Conference on Hybrid Systems: Computation and Control. pp. 189–198. IEEE (2015) https://doi.org/10.1145/2728606.2728633

  12. Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements for automotive systems. In: Proc. of ARCH@CPSWeek 2014: the 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. EPiC Series in Computing, 34, 25–30 (2015)

    Google Scholar 

  13. Jakšić, S., Bartocci, E., Grosu, R., Nguyen, T., Ničković, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53(1), 83–112 (2018). https://doi.org/10.1007/s10703-018-0319-x

    Article  MATH  Google Scholar 

  14. Jaksic, S., Bartocci, E., Grosu, R., Nickovic, D.: An algebraic framework for runtime verification. IEEE Trans. CAD Integr. Circ. Syst. 37(11), 2233–2243 (2018). https://doi.org/10.1109/TCAD.2018.2858460

    Article  Google Scholar 

  15. 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 

  16. Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Schramm, A.: Tessla: runtime verification of non-synchronized real-time streams. In: Proc. of SAC 2018: the 33rd Annual ACM Symposium on Applied Computing, pp. 1925–1933. ACM (2018) https://doi.org/10.1145/3167132.3167338

  17. Ma, M., Bartocci, E., Lifland, E., Stankovic, J.A., Feng, L.: SaSTL: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: 11th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2020, Sydney, Australia, April 21–25, 2020, pp. 51–62. IEEE (2020) https://doi.org/10.1109/ICCPS48487.2020.00013

  18. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

  19. Maler, O., Ničković, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)

    Article  Google Scholar 

  20. 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 

  21. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Logical Methods in Computer Science, 14(4) (2018) https://doi.org/10.23638/LMCS-14(4:2)2018

  22. Nenzi, L., Bortolussi, L., Loreti, M.: jSSTL - a tool to monitor spatio-temporal properties. In: Proc. of VALUETOOLS 2016: the 10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016, pp. 74–79. ACM (2016) https://doi.org/10.4108/eai.25-10-2016.2266978

  23. Beyer, D., Huisman, M. (eds.): TACAS 2018. LNCS, vol. 10806. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3

    Book  Google Scholar 

  24. Ratasich, D., Khalid, F., Geissler, F., Grosu, R., Shafique, M., Bartocci, E.: A roadmap towards resilient internet of things for cyber-physical systems. IEEE Access Early Access, 1–1 (2019) https://doi.org/10.1109/ACCESS.2019.2891969

  25. Rodionova, A., Bartocci, E., Ničković, D., Grosu, R.: Temporal logic as filtering. In: Proc. of HSCC 2016, pp. 11–20. ACM (2016) https://doi.org/10.1145/2883817.2883839

  26. Majumdar, R., Kunčak, V. (eds.): CAV 2017. LNCS, vol. 10426. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci & Laura Nenzi

  2. DMG, University of Trieste, Trieste, Italy

    Luca Bortolussi & Laura Nenzi

  3. University of Camerino, Camerino, Italy

    Michele Loreti

  4. Esteco S.p.A., Trieste, Italy

    Simone Silvetti

Authors
  1. Ezio Bartocci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Bortolussi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michele Loreti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Laura Nenzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Simone Silvetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Laura Nenzi .

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

Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L., Silvetti, S. (2020). MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties. 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_23

Download citation

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

  • 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