Formal Modeling of Hybrid System Based on Semi-continuous Colored Petri Net: A Case Study of Adaptive Cruise Control System

Many Next-Generation consumer electronic devices would be distributed hybrid electronic systems, such as UAVs (Unmanned Aerial Vehicles) and smart electronic cars. The safety and risk control are the key issues for the sustainability of such consumer electronic systems. The modeling of hybrid electronic systems is difficult to be abstracted by traditional Petri Nets. This also makes the reachable marking graph unable to be applied to Petri nets of the hybrid electronic systems. This paper proposes a novel Petri Net to model and analyze the hybrid electronic systems. We name it a Semi-continuous Colored Petri Net (SCPN) that inherits the excellent modeling capabilities and analysis methods of Petri Nets, and can formally depict hybrid quantities. In addition, we propose the construction algorithm for an SCPN reachable marking graph and prove its finiteness. Finally, we model and analyze an Adaptive Cruise Control (ACC) system of smart electronic cars as an example to prove the validity of SCPN. We use the proposed SCPN to model and analyze the running process of an ACC system under the continuous deceleration scenario of the front vehicle. The application study shows that the ACC system has logic flaws under the constant headway strategy when the front vehicle continues to decelerate. Based on this analysis, improvements to the SCPN of the ACC system are made, effectively enhancing its safety and logical correctness.