Stability Analysis of Nonlinear Systems Using Lyapunov Theories


Safety critical systems like autonomous driving or medical devices demand for powerful verification methodologies. Formal verification offers this opportunity. Howeverfor analog circuits and systems formal verification suffersfrom complexity and nonlinearity of underlying equationsin transistor models. Vera is a in-house tool used for equivalence checking and thus is a step to concur the verification task. The main concept of the algorithm lies in the sampling done in the state space. However, as the order of systems increase, the verification task becomes a challenge. Thus it would be beneficial if at least a statement about the stability of the system can be stated. This would have two effects: First, the stability of the system would be known. Thus proceeding to the verification only happens if the system is stable, as in most cases it's useless to verify an unstable system. Second, the examined region of the state space can now be specified or changed. This is of major importance as shown in.
This thesis aims to analyse the stability of a nonlinear system using Lyapunov theories


Using Lyapunov theories, the stability of a nonlinear system should be analyzed. Compared to the classical approach, this approach  utilizes the state space sampled points found by Vera. This means that since Vera discretized the state space, the values of the eigenvectors and eigenvalues are given for each point in the state space. Thus finding a descriptive Lyapunov function is an easier task.