[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Predicate monitoring in distributed cyber-physical systems

  • General
  • Special Issue: RV 2021
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

This paper solves the problem of detecting violations of predicates over distributed continuous-time and continuous-valued signals in cyber-physical systems (CPS). CPS often operate in a safety-critical context, where their correctness is crucially important. Large CPS that consist of many autonomous and communicating components distributed across a geographical area must maintain global correctness and safety. We assume a partially synchronous setting, where a clock synchronization algorithm guarantees a bound on clock drifts among all signals. We introduce a novel retiming method that allows reasoning about the correctness of predicates among continuous-time signals that do not share a global view of time. The resulting problem is encoded as an SMT problem and we introduce techniques to solve the SMT encoding efficiently. Leveraging simple knowledge of physical dynamics allows further runtime reductions. We fully implement our approach on three distributed CPS applications: monitoring of a network of autonomous ground vehicles, a network of aerial vehicles, and a water distribution system. The results show that in some cases it is even possible to monitor a distributed CPS sufficiently fast for online deployment on fleets of autonomous vehicles.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.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

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abbas, H., Mittelmann, H., Fainekos, G.: Formal property verification in a conformance testing framework. In: 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 155–164. IEEE (2014)

    Google Scholar 

  2. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Annapureddy, Y.S.R., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: a tool for temporal logic falsification for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 6605, pp. 254–257. Springer, Berlin (2011)

    Chapter  Google Scholar 

  4. Bauer, A., Falcone, Y.: Decentralised LTL monitoring. Form. Methods Syst. Des. 48(1–2), 46–93 (2016)

    Article  MATH  Google Scholar 

  5. Benndorf, M., Haenselmann, T.: Time synchronization on Android devices for mobile construction assessment. In: The Tenth International Conference on Sensor Technologies and Applications. Thinkmind (2016)

    Google Scholar 

  6. Bonakdarpour, B., Fraigniaud, P., Rajsbaum, S., Rosenblueth, D.A., Travers, C.: Decentralized asynchronous crash-resilient runtime verification. In: Proceedings of the 27th International Conference on Concurrency Theory (CONCUR), pp. 16:1–16:15 (2016)

    Google Scholar 

  7. Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Trans. Comput. Syst. 3(1), 63–75 (1985)

    Article  Google Scholar 

  8. Chauhan, H., Garg, V.K., Natarajan, A., Mittal, N.: A distributed abstraction algorithm for online predicate detection. In: Proceedings of the 32nd IEEE Symposium on Reliable Distributed Systems (SRDS), pp. 101–110 (2013)

    Google Scholar 

  9. Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Runtime Verification: 19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings, pp. 165–184. Springer (2019)

    Chapter  Google Scholar 

  10. Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. Form. Methods Syst. Des. 49(1–2), 109–158 (2016)

    Article  MATH  Google Scholar 

  11. Danielsson, L.M., Sánchez, C.: Decentralized stream runtime verification. In: Proceedings of the 19th International Conference on Runtime Verification (RV), pp. 185–201 (2019)

    Chapter  Google Scholar 

  12. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 337–340 (2008)

    Google Scholar 

  13. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Form. Methods Syst. Des. 51(1), 5–30 (2017)

    Article  MATH  Google Scholar 

  14. Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Runtime Verification: 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings 5, pp. 231–246. Springer, Berlin (2014)

    Chapter  Google Scholar 

  15. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 92–106 (2010)

    Chapter  MATH  Google Scholar 

  16. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Proceedings of the 25th International Conference on Computer Aided Verification (CAV), pp. 264–279 (2013)

    Chapter  Google Scholar 

  17. Drone Life: FAA UTM project: Decentralized UAS traffic management demonstration, September 2019. https://dronelife.com/2019/09/09/decentralized-uas-traffic-management-demonstration

  18. FAA. DOT UAS initiatives, April 2019. https://www.faa.gov/uas/programs_partnerships/DOT_initiatives

  19. Fainekos, G.E., Pappas, G.J.: Robust sampling for MITL specifications. In: Proceedings of 5th International Conference on the Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 147–162 (2007)

    Chapter  Google Scholar 

  20. Fraigniaud, P., Rajsbaum, S., Travers, C.: Locality and checkability in wait-free computing. Distrib. Comput. 26(4), 223–242 (2013)

    Article  MATH  Google Scholar 

  21. Fraigniaud, P., Rajsbaum, S., Travers, C.: A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring. J. Appl. Comput. Topol. 4(1), 141–179 (2020)

    Article  MathSciNet  MATH  Google Scholar 

  22. Ganguly, R., Momtaz, A., Bonakdarpour, B.: Distributed runtime verification under partial asynchrony. In: Proceedings of the 24th International Conference on Principles of Distributed Systems (OPODIS), pp. 20:1–20:17 (2020)

    Google Scholar 

  23. Garg, V.K., Chase, C.: Distributed algorithms for detecting conjunctive predicates. In: International Conference on Distributed Computing Systems, pp. 423–430 (1995)

    Google Scholar 

  24. Hendry-Brogan, M.: Global unmanned aerial vehicle (UAV) market report. Technical report, Technical report (May 2019)

  25. Kazemloo, S., Bonakdarpour, B.: Crash-resilient decentralized synchronous runtime verification. In: Proceedings of the 37th Symposium on Reliable Distributed Systems (SRDS), pp. 207–212 (2018)

    Google Scholar 

  26. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  27. Medhat, R., Bonakdarpour, B., Kumar, D., Fischmeister, S.: Runtime monitoring of cyber-physical systems under timing and memory constraints. ACM Trans. Embed. Comput. Syst. 14(4), 79:1–79:29 (2015)

    Article  Google Scholar 

  28. Mills, D.: Network time protocol version 4: Protocol and algorithms specification. RFC 5905, RFC Editor, June 2010

  29. Mittal, N., Garg, V.K.: Techniques and applications of computation slicing. Distrib. Comput. 17(3), 251–277 (2005)

    Article  MATH  Google Scholar 

  30. Momtaz, A., Basnet, N., Abbas, H., Bonakdarpour, B.: Predicate monitoring in distributed cyber-physical systems. In: Proceedings of the 21st International Conference on Runtime Verification (RV), pp. 3–22 (2021)

    Chapter  Google Scholar 

  31. Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of the 29th IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 494–503 (2015)

    Google Scholar 

  32. National Science Foundations: Revolutionizing how we keep track of time in cyber-physical systems, June 2014. https://nsf.gov/news/news_summ.jsp?cntn_id=131691

  33. Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Proceedings of the 21st International Symposium on Distributed Computing (DISC), pp. 420–434 (2007)

    MATH  Google Scholar 

  34. Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: 2017 IEEE Conference on Control Technology and Applications (CCTA), pp. 1235–1240. IEEE (2017)

    Chapter  Google Scholar 

  35. Pereira, J.C., Machado, N., Sousa Pinto, J.: Testing for race conditions in distributed systems via SMT solving. In: International Conference on Tests and Proofs, Bergen, Norway, June 22–26, 2020, Proceedings, pp. 122–140 (2020)

    Google Scholar 

  36. Quesel, J.-D.: Similarity, logic, and games: bridging modeling layers of hybrid systems. PhD thesis, Carl Von Ossietzky Universität Oldenburg (July 2013)

  37. Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: Proceedings. 26th International Conference on Software Engineering, pp. 418–427. IEEE (2004)

    Chapter  Google Scholar 

  38. Tekken Valapil, V., Yingchareonthawornchai, S., Kulkarni, S.S., Torng, E., Demirbas, M.: Monitoring partially synchronous distributed systems using SMT solvers. In: Runtime Verification – 17th International Conference, RV 2017, Seattle, WA, USA, September 13–16, 2017, Proceedings, pp. 277–293 (2017)

    Google Scholar 

  39. USNRC: Emergency core cooling systems, March 2021. https://www.nrc.gov/docs/ML1122/ML11223A220.pdf

  40. USNRC: Pressurized water reactor systems, March 2021. https://www.nrc.gov/reading-rm/basic-ref/students/for-educators/04.pdf

  41. Zhang, X., Leucker, M., Dong, W.: Runtime verification with predictive semantics. In: NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3–5, 2012. Proceedings 4, pp. 418–432. Springer (2012)

    Chapter  Google Scholar 

Download references

Acknowledgements

This work is sponsored in part by the United States NSF FMitF-2102106 and CCF (SHF)-2118356 awards.

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, Michigan State University, East Lansing, 48824, MI, USA

    Anik Momtaz & Borzoo Bonakdarpour

  2. School of Electrical Engineering and Computer Science, Oregon State University, Corvallis, 97331, OR, USA

    Niraj Basnet & Houssam Abbas

Authors
  1. Anik Momtaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Niraj Basnet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Houssam Abbas
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Anik Momtaz, Houssam Abbas or Borzoo Bonakdarpour.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Momtaz, A., Basnet, N., Abbas, H. et al. Predicate monitoring in distributed cyber-physical systems. Int J Softw Tools Technol Transfer 25, 541–556 (2023). https://doi.org/10.1007/s10009-023-00718-x

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-023-00718-x

Keywords

Search

Navigation