Advertisement

Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries

  • Hojat KhosrowjerdiEmail author
  • Hamed Nemati
  • Karl Meinke
Conference paper
  • 38 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12165)

Abstract

We explore the application of graph database technology to spatio-temporal model checking of cooperating cyber-physical systems-of- systems such as vehicle platoons. We present a translation of spatio-temporal automata (STA) and the spatio-temporal logic STAL to semantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem to graph database query solving. The practicability and efficiency of this approach is evaluated by introducing NeoMC, a prototype implementation of our explicit model checking approach based on Neo4j. To evaluate NeoMC we consider case studies of verifying vehicle platooning models. Our evaluation demonstrates the effectiveness of our approach in terms of execution time and counterexample detection.

Notes

Acknowledgments

This research has been supported by KTH ICT-TNG project STaRT (Spatio-Temporal Planning at Runtime), as well as the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762).

References

  1. 1.
    Khosrowjerdi, H., Meinke, K.: Learning-based testing for autonomous systems using spatial and temporal requirements. In: Proceedings of the 1st International Workshop on Machine Learning and Software Engineering in Symbiosis, MASES@ASE 2018, Montpellier, France, 3 September 2018, pp. 6–15 (2018).  https://doi.org/10.1145/3243127.3243129
  2. 2.
    Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 18–36. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-12988-0_2CrossRefGoogle Scholar
  3. 3.
    Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. Theor. Comput. Sci. 744, 143–169 (2018).  https://doi.org/10.1016/j.tcs.2018.05.028MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994).  https://doi.org/10.1016/0304-3975(94)90010-8MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Chaochen, Z., Hoare, C., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991). http://www.sciencedirect.com/science/article/pii/002001909190122XMathSciNetCrossRefGoogle Scholar
  6. 6.
    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: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14–16 April 2015, pp. 189–198 (2015). https://doi.org/10.1145/2728606.2728633
  7. 7.
    Quesel, J.-D., Schäfer, A.: Spatio-temporal model checking for mobile real-time systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 347–361. Springer, Heidelberg (2006).  https://doi.org/10.1007/11921240_24CrossRefGoogle Scholar
  8. 8.
    Angles, R., Arenas, M., Barceló, P., Hogan, A., Reutter, J.L., Vrgoc, D.: Foundations of modern query languages for graph databases. ACM Comput. Surv. 50(5), 68:1–68:40 (2017). http://doi.acm.org/10.1145/3104031CrossRefGoogle Scholar
  9. 9.
    Bennaceur, A., Hähnle, R., Meinke, K. (eds.): Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96562-8CrossRefGoogle Scholar
  10. 10.
    Meinke, K., Niu, F.: A learning-based approach to unit testing of numerical software. In: Petrenko, A., Simão, A., Maldonado, J.C. (eds.) ICTSS 2010. LNCS, vol. 6435, pp. 221–235. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16573-3_16CrossRefGoogle Scholar
  11. 11.
    Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 134–151. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21768-5_11CrossRefGoogle Scholar
  12. 12.
    Webber, J.: A programmatic introduction to neo4j. In: Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH 2012, Tucson, AZ, USA, 21–25 October 2012, pp. 217–218 (2012). https://doi.org/10.1145/2384716.2384777
  13. 13.
    Francis, N., et al.: Cypher: an evolving query language for property graphs. In: Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, 10–15 June 2018, pp. 1433–1445 (2018). http://doi.acm.org/10.1145/3183713.3190657
  14. 14.
    de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, (2010). iv + 417 pages, Machine Translation, vol. 24, no. 3–4, pp. 291–293, 2010. https://doi.org/10.1007/s10590-011-9086-9
  15. 15.
    Angles, R., Gutiérrez, C.: Survey of graph database models. ACM Comput. Surv. 40(1), 11–139 (2008).  https://doi.org/10.1145/1322432.1322433CrossRefGoogle Scholar
  16. 16.
    Robinson, I., Webber, J., Eifrem, E.: Graph Databases: New Opportunities for Connected Data, 2nd edn. O’Reilly Media Inc., Sebastopol (2015)Google Scholar
  17. 17.
    Hölsch, J., Schmidt, T., Grossniklaus, M.: On the performance of analytical and pattern matching graph queries in neo4j and a relational database. In: Proceedings of the Workshops of the EDBT/ICDT 2017 Joint Conference (EDBT/ICDT 2017), Venice, Italy, 21–24 March 2017 (2017). http://ceur-ws.org/Vol-1810/GraphQ_paper_01.pdf
  18. 18.
    Francis, N., et al.: Formal semantics of the language cypher. CoRR, vol. abs/1802.09984 (2018). http://arxiv.org/abs/1802.09984
  19. 19.
    Junghanns, M., Kießling, M., Averbuch, A., Petermann, A., Rahm, E.: Cypher-based graph pattern matching in gradoop. In: Proceedings of the Fifth International Workshop on Graph Data-management Experiences & Systems, GRADES@SIGMOD/PODS 2017, Chicago, IL, USA, 14–19 May 2017, pp. 3:1–3:8 (2017). http://doi.acm.org/10.1145/3078447.3078450
  20. 20.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8CrossRefzbMATHGoogle Scholar
  21. 21.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: 24th Annual Symposium on Foundations of Computer Science, Tucson, Arizona, USA, 7–9 November 1983, pp. 185–194 (1983). https://doi.org/10.1109/SFCS.1983.51
  22. 22.
    Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985).  https://doi.org/10.1016/0020-0190(85)90056-0MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, June 16–18, 1986, pp. 332–344 (1986)Google Scholar
  24. 24.
    Búr, M., Szilágyi, G., Vörös, A., Varró, D.: Distributed graph queries for runtime monitoring of cyber-physical systems. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 111–128. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89363-1_7CrossRefGoogle Scholar
  25. 25.
    Meinke, K.: Learning-based testing of cyber-physical systems-of-systems: a platooning study. In: Reinecke, P., Di Marco, A. (eds.) EPEW 2017. LNCS, vol. 10497, pp. 135–151. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66583-2_9CrossRefGoogle Scholar
  26. 26.
    Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_22CrossRefGoogle Scholar
  27. 27.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Referencemanual. Addison-Wesley, Boston (2004)Google Scholar
  28. 28.
    Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_61CrossRefGoogle Scholar
  29. 29.
    Chiarugi, D., Falaschi, M., Hermith, D., Olarte, C.: Verification of spatial and temporal modalities in biochemical systems. Electr. Notes Theor. Comput. Sci. 316, 29–44 (2015).  https://doi.org/10.1016/j.entcs.2015.06.009CrossRefzbMATHGoogle Scholar
  30. 30.
    Parvu, O., Gilbert, D.R.: Automatic validation of computational models using pseudo-3D Spatio-temporal model checking. BMC Syst. Biol. 8, 124 (2014).  https://doi.org/10.1186/s12918-014-0124-0CrossRefGoogle Scholar
  31. 31.
    Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009).  https://doi.org/10.1145/1467247.1467271CrossRefzbMATHGoogle Scholar
  32. 32.
    de Oliveira, Í.R., Cugnasca, P.S.: Checking safe trajectories of aircraft using hybrid automata. In: Anderson, S., Felici, M., Bologna, S. (eds.) SAFECOMP 2002. LNCS, vol. 2434, pp. 224–235. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45732-1_22CrossRefGoogle Scholar
  33. 33.
    Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 297–311. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-49224-6_24CrossRefGoogle Scholar
  34. 34.
    Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. STTT 20(3), 289–311 (2018).  https://doi.org/10.1007/s10009-018-0483-8CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.KTH Royal Institute of TechnologyStockholmSweden
  2. 2.Helmholtz Center for Information Security (CISPA)SaarbrückenGermany

Personalised recommendations