Abstract

Signal-flow-graph theory provides an efficient framework to model various engineering and physical systems at a higher-level of abstraction. In this paper, we present the formalization of the signal-flow-graph theory with an ultimate goal to conduct the formal analysis of engineering systems within a higher-order-logic theorem prover. In particular, our formalization can tackle system models which are based on undirected graphs. We also present the formalization of the system transfer function and associated properties such as stability and resonance. In order to demonstrate the effectiveness our work, we present the formal analysis of two engineering systems namely PANDA Vernier resonator and z-source impedance network, which are commonly used in photonics and power electronics, respectively.