Verification of balancing architectures for modular batteries

Large battery packs consisting of a high number of cells are essential in electric vehicles as well as in smart grids as stationary energy buffers. In this context, active cell balancing techniques improve the lifetime and capacity of battery packs significantly by equalizing charge at runtime. Modern balancing circuits rely on switching schemes to transfer charge between cells via energy storage elements such as inductors or capacitors. Verifying correct functionality of complex architectures can become a non-trivial task where circuit and control have to be considered concurrently. For this purpose, we provide a framework for the verification of balancing architectures, using a methodology that takes advantage of graph search algorithms. While this paper focuses on inductor-based architectures, the proposed approach might also be extended to other storage elements such as capacitors or transformers. The experimental results based on several case studies give evidence that a manual verification becomes impractical and our framework is capable of either proving correctness or delivering a counter-example.