### Imhotep-SMT

#### Novel SMT solver for secure state estimation

## Example 1: Securing an Unmanned Ground Vehicle

This is an example of using Imhotep-SMT in estimating the state of an Unmanned Ground Vehicle (UGV) while one of its sensors is under attack.

The Matlab files for this example can be downloaded from here.

## Example 2: Active Cruise Control

In this example, we show how Imhotep-SMT can be used to securely estimating the state of a driving car while performing active cruise control. The simulation consists of two leader cars followed by two followers cars. The follower cars are under sensor attacks. One of the cars (blue) uese Imhotep-SMT to estimate the state while the other follower car (red) uses standard least squares estimator. The simulation uses a 3D virtual reality simulator to show the perfromance of the two estimators. The simulation is currently restricted to the case when the cars are driving in straight lines.

The Matlab files for this example can be downloaded from here.

## Example 3: IEEE 14-bus Power Grid

This is an example of using Imhotep-SMT in estimating the state of the IEEE 14-bus power network. The bus composed of 5 synchronous generators and 14 buses. The state of each generator includes rotor angle and frequency. The overall system has 35 sensors: 14 sensors measure the real power injections at every bus, 20 sensors measure the real power flows along every branch, and one sensor measures the rotor angle of generator number 1. In this simulation, the attacker is assumed to pick a random set of 14 sensors. We compare the efficiency of Imohtep-SMT by comparing its estimation error with respect to the estimation error of a classical least squares estimator.

The Matlab files for this example can be downloaded from here.

## Example 4: Random, Large Scale Systems

To assess the scalability of Imhotep-SMT, we randomly generated a set of matrices for systems of increasing size. For each of these systems, we configured Imohtep-SMT, provided it with the system inputs and outputs for state estimation, and recorded the execution time. In the first experiment, we fix the number of sensors $p = 20$ and increase the number of system states from $n = 10$ to $n = 150$. In the second experiment, we fix the number of states n=50 and increase instead the number of sensors from $p = 3$ to $p = 150$. In both cases, half of the sensors are attacked. As a result, increasing n has a small effect on the overall execution time, which reflects the fact that the number of constraints to be satisfied does not depend on $n$. Conversely, as the number of sensors increases, the number of constraints increases, hence the execution time of Imhotep-SMT.

The Matlab files for this example can be downloaded from here.