A formal model for temporal - Spatial event in internet of vehicles

Abstract

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.