LAUSR

An ordinary-differential-equation (ODE) enabled reachable dynamics analysis approach is devised to provably enclose all possible dynamic trajectories of networked microgrids (NMs) under both uncertain renewable power injections and intermittent large disturbance events. As a formal verification tool for the NM dynamics, its new contributions are threefold: 1) An ODE-enabled NMs model is established with a thorough formulation of the hierarchical control of DERs as well as the network transients; 2) A hybrid automaton method is established to empower the reachability analysis of dynamic transitions in NMs caused by arbitrary large disturbances; 3) A zonotope bundle technique is introduced in the reachable set calculation to capture the fast transients and strong nonlinearity upon the occurrence of disturbances, which allows for the reliable formal verification with superior precision and convergence performance. Extensive case studies are performed to demonstrate the effectiveness of the new approach in formally verifying the dynamical performance of disturbed NMs equipped with hierarchical inverter control.