Control software often executes on common embedded platforms to achieve the number of safety-critical tasks. These concurrent running tasks introduce variability in the response time of the controller software. Timing effects like sampling-jitter and actuation delay, though critical to the safety of the closed-loop system, are often ignored during design and analysis. There are several well established tools present for verification of hybrid systems. But very few tools which consider these perturbations when a control program runs in closed loop with some plant. None of them considers controller program along with non-linear plant and timing effects altogether while verifying safety of the closed loop. That’s why as part of this work, a tool is to be designed, that considers Plant dynamics (ODEs), Controller program and noise, jitters and delays caused by the closed loop formation to verify if the closed loop system holds desired safety criteria. Non-Linear Systems are also considered, as the solver intended to be used supports them. This helps industries employing safety-critical embedded software certify if the controller is safe when connected in closed loop with a plant model.

We have developed methods to find security loopholes by analysing safety of these systems as they continue to function in real world. This analysis helps understand how robust the control system is towards such anomalies. Using this approach, we can as well understand how an attacker functions and make it more realistic by imposing real-world constraints. We can intelligently mine these system parameters that can restraint the accessibility of system vulnerabilities. Along with analyzing vulnerabilities we are also interested in system control behaviours and how are those affected when such attack scenarios arise in real world. As we are interested in provably secure such systems, we utilize several verification tools like Z3, dReal to analyse system vulnerabilities.