Formal Verification of Safety- Critical EV Charging Control Systems

Abstract

Electric vehicle charging systems are becoming increasingly safety-critical as charger control logic must respond correctly to overload, fault, shutdown, and recovery conditions under automated operation. Existing studies on charging safety, secure charging coordination, and control assurance highlight the growing need for rigorous validation, yet formal verification of EV charging control behavior remains limited compared with conventional testing and simulation-based evaluation. This gap is important because unsafe state transitions or hidden control-path errors can persist even when a controller appears correct during nominal operation. This article presents a formal verification framework for safety-critical EV charging control systems based on state-transition modeling, temporal logic safety properties, model checking, and counterexample-guided control refinement. The results show that the verified controller achieves strong verification success, high property satisfaction, broad fault detection coverage, and effective elimination of unsafe transitions across multiple charging control scenarios. The study demonstrates that formal verification can provide a rigorous and practical foundation for trustworthy EV charging control design.