Modeling and Analysis of ETC Control System with Colored Petri Net and Dynamic Slicing

What is it about?

Nowadays, an Electronic Toll Collection (ETC) control system in highways has been widely adopted to smoothen traffic flow. However, as it is a complex business interaction system, there are inevitably flaws in its control logic process, such as the problem of vehicle fee evasion. Even we find that there are more than one way for vehicles to evade fees. This shows that it is difficult to ensure the completeness of its design. Therefore, it is necessary to adopt a novel formal method to model and analyze its design, detect flaws, and modify it. In this paper, a Colored Petri net (CPN) is introduced to establish its model. To analyze and modify the system model more efficiently, a dynamic slicing method of CPN is proposed. First, a static slice is obtained from the static slicing criterion by backtracking. Second, considering all binding elements that can be enabled under the initial marking, a forward slice is obtained from the dynamic slicing criterion by traversing. Third, the dynamic slicing of CPN is obtained by taking the intersection of both slices. The proposed dynamic slicing method of CPN can be used to formalize and verify the behavior properties of an ETC control system, and the flaws can be detected effectively. As a case study, the flaw of a vehicle that has not completed the payment following the previous vehicle passing the railing is detected by the proposed method.

Featured Image

Photo by Possessed Photography on Unsplash

Photo by Possessed Photography on Unsplash

Why is it important?

1.We propose a formal modeling method based on CPN for the control logic process of an ETC control system, and take a case study which derived from real scenes as an example to illustrate the modeling process. 2.We propose a dynamic slicing method for CPN. This method can reduce the size of the CPN model and reduce the size of state spaces of the model, which can be used to detect the flaws in ETC control logic process. 3.We illustrate how to analyze whether there are logic flaws in the ETC control system model, i.e., faulty states for vehicle fee evasion. As a case study, we detect whether there is a flaw that the vehicle that has not completed the payment passing the railing by following the previous vehicle in the ETC control system, and give a specific modification plan.

Perspectives