Formal approaches to design of active cell balancing architectures in battery management systems

Large battery packs composed of Lithium-Ion cells are continuously gaining in importance due to their applications in Electric Vehicles (EVs) and smart energy grids. To ensure maximum lifetime, safety and performance of the battery pack, complex embedded system architectures consisting of sensors, power electronics and microcontrollers are integrated into the pack as Battery Management System (BMS). In this context, active cell balancing is a promising approach of the BMS to provide equal charge levels across the cells in the battery pack in an efficient manner. The design of such active cell balancing architectures, comprising circuits from the power electronics domain together with complex control schemes, is error-prone and tedious when done in the conventional manual fashion. This paper presents a design flow from a high-level requirements definition to an actual hardware implementation, using design automation approaches such as verification, synthesis and optimization. Here, graph-based models and algorithms from the domain of formal verification are applied to prove the system properties and are extended to enable synthesis of optimized and correct-by-construction active balancing circuit architectures.