Statistical verification techniques for stochastic dynamic systems

Abstract

Electronic chip design, aircraft stability, finance, economy and even our social life can be affected by random events. Noise is a random process that occurs due to unwanted signal interactions in electronic circuits and environmental phenomena such as thunder, manufacturing defects or thermal increment. Noise affects the performance of our design and will cause unpredictable results on the output of the system. Consequently, we need to model noise and analyze the system at its presence. Verifying the performance of a dynamic system in the presence of noise requires a highly complicated mathematical skills. There are different verification techniques that rely on impractically expensive techniques. Flight dynamics characterizes the response of an aircraft vehicle to its control inputs, gravitational forces, and perturbations and has to adhere to strict design and safety requirements. In this thesis, we are interested in modeling and verifying the stability of aircrafts such as F4 in presence of noise. In order to study the random behavior of noise, we propose an approach based on modeling the designs using stochastic differential equations (SDE) in the time domain. Furthermore, we propose a modeling and estimation methodology that allows us to capture the perturbation in the form of Stochastic Differential Equations for the statistical monitoring of the stability property. Finally, pattern matching and Monte Carlo based verification methods are used for qualitative estimation of the simulation traces.