Yu, Wangyang and Kong, Jinming and Ding, Zhijun and Zhai, Xiaojun and Li, Zhiqiang and Guo, Qi (2024) Modeling and Analysis of ETC Control System with Colored Petri Net and Dynamic Slicing. ACM Transactions on Embedded Computing Systems, 23 (1). pp. 1-27. DOI https://doi.org/10.1145/3633450
Yu, Wangyang and Kong, Jinming and Ding, Zhijun and Zhai, Xiaojun and Li, Zhiqiang and Guo, Qi (2024) Modeling and Analysis of ETC Control System with Colored Petri Net and Dynamic Slicing. ACM Transactions on Embedded Computing Systems, 23 (1). pp. 1-27. DOI https://doi.org/10.1145/3633450
Yu, Wangyang and Kong, Jinming and Ding, Zhijun and Zhai, Xiaojun and Li, Zhiqiang and Guo, Qi (2024) Modeling and Analysis of ETC Control System with Colored Petri Net and Dynamic Slicing. ACM Transactions on Embedded Computing Systems, 23 (1). pp. 1-27. DOI https://doi.org/10.1145/3633450
Abstract
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 about a vehicle that has not completed the payment following the previous vehicle to pass the railing is detected by the proposed method.
Item Type: | Article |
---|---|
Uncontrolled Keywords: | Colored Petri net; ETC control system; dynamic slicing; formalized analysis |
Divisions: | Faculty of Science and Health Faculty of Science and Health > Computer Science and Electronic Engineering, School of |
SWORD Depositor: | Unnamed user with email elements@essex.ac.uk |
Depositing User: | Unnamed user with email elements@essex.ac.uk |
Date Deposited: | 24 Jan 2024 11:17 |
Last Modified: | 07 Aug 2024 16:09 |
URI: | http://repository.essex.ac.uk/id/eprint/37628 |
Available files
Filename: 52163642_File000000_1285861895.pdf