A Formal Model for Temporal - Spatial Event in Internet of Vehicles

  • Na WangEmail author
  • Xuemin Chen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11280)


In internet of vehicles (IoV), there are several events, e.g., location, speed, arriving time, that should be detected while the vehicle is running. Nowadays, formal description is becoming an effective method to describe and detect events. In this paper, we propose a temporal - spatial Petri net (TSPN) formal model which is deduced from Petri net. The rules of transition firing and marking updating are both defined in TSPN for further system analysis. In addition, an efficient TSPN analysis algorithm is developed for structured detection models. With a case study, we illustrate that TSPN can describe and detect events in advance for the IoV system.


Formal model Temporal and spatial Petri net Internet of vehicles Event detection 


  1. 1.
    JGerla, M., Lee, E., Pau, G.: Internet of vehicles: from intelligent grid to autonomous cars and vehicular clouds. In: 2015 IEEE World Forum, pp. 241–246. IEEE, Seoul (2014)Google Scholar
  2. 2.
    Bosman, H., Iacca, G., Tejada, A., Heinrich, J.: Spatial anomaly detection in sensor networks using neighborhood information. Inf. Fusion 33(1), 41–56 (2017)CrossRefGoogle Scholar
  3. 3.
    Kang, M., Yu, H., Xiong, Q., Hu, H.: Spatial-temporal correlative fault detection in wireless sensor networks. Int. J. Distrib. Sens. Netw. 2014, 1–16 (2015)Google Scholar
  4. 4.
    Man, K., Krilaviius, T., Vallee, T., Leung, H.: A formal analysis tool for wireless sensor networks. Int. J. Res. Rev. Comput. Sci. 1, 24–26 (2009)Google Scholar
  5. 5.
    Liu, K., Lin, H., Fei, Z., Liang, J.: Spatially-temporally online fault detection using timed multivariate statistical logic. Eng. Appl. Artif. Intell. 65(1), 51–59 (2017)CrossRefGoogle Scholar
  6. 6.
    Olveczky, P., Thorvaldsen, S.: Formal modeling and analysis of wireless sensor network algorithms in real-time Maude. In: 20th IEEE International Parallel and Distributed Processing Symposium, pp. 122–140. IEEE, Rhodes Island, Greece (2007)Google Scholar
  7. 7.
    Agha, G., Meseguer, J., Sen, K.: Maude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRefGoogle Scholar
  8. 8.
    Riaza, S., Afzaala, H.: Formalizing mobile ad hoc and sensor networks using VDM-SL. Procedia Comput. Sci. 63, 148–153 (2015)CrossRefGoogle Scholar
  9. 9.
    Silva, D.S., Resner, D., de Souza, R.L., Martina, J.E.: Formal verification of a cross-layer, trustful space-time protocol for wireless sensor networks. In: Ray, I., Gaur, M.S., Conti, M., Sanghi, D., Kamakoti, V. (eds.) ICISS 2016. LNCS, vol. 10063, pp. 426–443. Springer, Cham (2016). Scholar
  10. 10.
    Testa, A., Cinque, M., Coronato, A., De, P., Augusto, J.: Heuristic strategies for assessing wireless sensor network resiliency: an event-based formal approach. J. Heuristics 21(2), 145–175 (2015)CrossRefGoogle Scholar
  11. 11.
    Wang, J., Li, D.: Resource oriented workflow nets and workflow resource requirement analysis. Int. J. Softw. Eng. Knowl. Eng. 23(5), 677–693 (2013)CrossRefGoogle Scholar
  12. 12.
    Tremblay, M.: Cutkosky.: Using sensor fusion and contextual information to perform event detection during a phase-based manipulation task. In: IEEE International Conference on Intelligent Robots and Systems, pp. 262–267. IEEE, Pittsburgh (1995)Google Scholar
  13. 13.
    Kapitanova, K., Sang, H.: A compact event description and analysis language for wireless sensor networks. In: 2009 Sixth International Conference on Networked Sensing Systems, pp. 1–4. IEEE Computer Society, Pittsburgh (2009)Google Scholar
  14. 14.
    Xiao, Q.: Bus Plan Research Based on GPS Data. Beijing Jiaotong University, Beijing (2009)Google Scholar
  15. 15.
    Guo, S., Wei, Y., Shi, W.: The statistics analysis of bus stop time. J. Gungxi Normal Univ. 24(2), 5–9 (2006)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Shanghai Polytechnic UniversityShanghaiChina
  2. 2.Texas Southern UniversityHoustonUSA

Personalised recommendations