Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing

Sometimes we only have access to a pre-collected training data set. LearnContract can be modified to accommodate this setup. Given the number of samples $n$ and $pr$, $\delta$, according to Proposition 2, we can get an upper bound on the gap $\epsilon$ and therefore get a lower bound for the empirical conformance $\hat{p}$. We can then use quantile regression to find the contract with right empirical conformance on the training data set.

LearnContract constructs candidate perception contracts that are conformant to a degree, over specified state $\tilde{X}$ and environment $\tilde{E}$ spaces. For certain environments $e\in\tilde{E}$, the system $S$ may not meet the requirements, and therefore, the most precise and conformant candidate contracts computed over such an environment $e$ will not be correct. In Section 4.2, we will develop techniques for refining $\tilde{X}$ and $\tilde{E}$ to find contracts that are correct or find counter-examples. For the completeness of this search process we will make the following assumption about convergence of LearnContract with respect to $\tilde{E}$.

Consider a monotonically decreasing sequence of sets $\{E_{k}\}_{n=1}^{\infty}$, such that their limit $\liminf_{k\rightarrow\infty}E_{k}=\{e_{d}\}$ for some environment $e_{d}\in\tilde{E}$. Let $\{M_{k}\}$ be the corresponding sequence of candidate contracts constructed by LearnContract for changing $\tilde{E}=E_{k}$, while keeping all other parameters fixed. We will say that the algorithm is convergent at $e_{d}$ if for all $x\in\tilde{X},\liminf_{k\rightarrow\infty}M_{k}(x)=\hat{h}(x,e_{d}).$ Informally, as candidate contracts are computed for a sequence of environments converging to $e_{d}$, the contracts point-wise converge to $\hat{h}$. In Section 5, we will see examples providing empirical evidence for this convergence property.

computes an over-approximation of ${Reach}_{S_{M}}(t)$ of the system $S_{{M}}=\langle\tilde{X},X_{c},Y,\tilde{E},f,M_{\tilde{E}}\rangle$. For showing completeness of the algorithm, we assume that Reach converges to a single execution as $X_{c}$, $\tilde{E}$ converges to a singleton set. This assumption is satisfied by many reachability algorithms, especially simulation-based reachability algorithms [9, 24].

takes as input a set of states, and partitions it into a finer set of states. With enough refinements, all partitions will converge to arbitrarily small sets. There are many strategies for refining state partitions, such as, bisecting hyperrectangular sets along coordinate axes.

The ShrinkEnv function takes as input a set of environmental parameters $\tilde{E}$, the nominal environmental parameter $e_{d}$, ${M}_{\tilde{E}}$ and the actual perception function ${\hat{h}}$ and generates a new set of environmental parameters. The sequence of sets generated by repeatedly apply ShrinkEnv will monotonically converge to a singleton set containing only the nominal environmental parameter $e_{d}$.

The dynamics ($f$) combines the physics model of the aircraft with a controller that follows a nominal trajectory. A 6-dimensional nonlinear differential equation describes the motion of the aircraft with yaw rate $\beta$, the pitch rate $\omega$, and acceleration $a$ as the control inputs (Details are given in the Appendix). The aircraft controller tries to follow a reference trajectory $\xi_{r}:\mathbb{Z}^{\geq 0}\rightarrow X$ approaching the runway. This reference approach trajectory starts at position $2.3$ kilometers from the touchdown point and $120$ meters above ground, and has a $-3^{\circ}$ slope in the z direction. The reference approach has constant speed of $10m/s$.

The observations $\langle\hat{x},\hat{y},\hat{z},\hat{\psi},\hat{\theta}\rangle$ are computed using a realistic perception pipeline composed of three functions (Fig. 1): (1) The airplane’s front camera generates an image, (2) a key-point detector detects specific key-points on the runway in that image using U-Net [20], (3) pose estimator uses the detected key-points and the prior knowledge of the actual positions of those key-points on the ground, to estimate the pose of the aircraft. This last calculation is implemented using the perspective-n-point algorithm [10]. Apart from the impact of the environment on the image, the observer is deterministic.

For this paper, we study the effects of two dominant environment factors, namely the ambient light and the position of the sun, represented by a spotlight¹¹1We have also performed similar analysis with fog and rain, but the discussion is not included here owing to limited space.. (1) The ambient light intensity in the range [0.2, 1.2] and (2) the spot light’s angle (with respect to the runway) in the range $[-0.1,0.6]$ radians, define the environment $E_{0}$. These ranges are chosen to include a nominal environment $e_{d}=\langle 1.0,0\rangle$ in which there exists an initial state $x_{0}\in X_{0}$ from which the system is safe. Sample camera images from the same state under different environmental conditions are shown in Fig. 1.

To compute the perception contract, we choose the desired conformance $pr=90\%$, the gap between actual conformance and empirical conformance $\epsilon=1\%$ and the confidence parameter $\delta=0.1\%$. From LearnContract, the empirical conformance measure should be at least $91\%$ for approximately $34$K samples. We round this up to $40$k samples. The computed perception contract ${M}_{\tilde{E}}$ achieves $92.4\%$ empirical conformance measure over $\tilde{E}$.

Additionally, we run 30 random simulations from $X_{01}$ under $\tilde{E}$. Out of the resulting $30$K data points generated, $29590$ observations were contained in the computed perception contract $M$, which gives an empirical conformance of $98.6\%$ for this different sampling distribution. This shows that ${M}_{\tilde{E}}$ meets the desired conformance and can be even better for some realistic sampling distributions.

The set of environmental parameters $\tilde{E}$ found by DaRePC also reveals some interesting behavior of the perception pipeline. We can see from Fig. 2 that when the intensity of ambient light is below 0.6 or above 1.15, the performance of perception pipeline becomes bad as many of the partitions are removed in those region. However, we can see there is a region $[0.95,1.1]\times[0.25,0.4]$ where the ambient lighting condition is close to the nominal ambient lighting condition, but surprisingly, the performance of perception pipeline is still bad. We found that this happens because in this environment, the glare from the spotlight (sun) makes the runway too bright for the perception pipeline to detect keypoints. Conversely, in region $[0.4,0.6]\times[0.25,0.4]$, the relatively low ambient light is compensated by the sun, and therefore, the perception pipeline has reliable performance for landing.

Fig. 2 shows the system-level safety requirement ${R}$ in blue and $\textsc{Reach}(X_{01},{M}_{\tilde{E}},t)$ in red. We can see that the computed reachable set indeed falls inside ${R}$, which by Proposition 1, implies that if the perception pipeline $\hat{h}$ conforms to ${M}_{\tilde{E}}$ then $\langle{\hat{h}},X_{01},\tilde{E}\rangle\models{R}$.

Further, to check $\langle{\hat{h}},X_{01},\tilde{E}\rangle\models{R}$, we run 30 simulations starting from states randomly sampled from $X_{01}$ under environments randomly sampled from $\tilde{E}$. The results are shown in Fig. 2. All 30 simulations satisfy ${R}$, and only one of these is not in the computed reachable set. This happens because ${M}_{\tilde{E}}$ doesn’t have $100\%$ conformance, and therefore cannot capture all behaviors of the actual system.

We performed 10 random simulations from $X_{01}$ under $E_{0}\setminus\tilde{E}$. Eight out of the 10 violate ${R}$ (Red trajectories in Fig. 2). This suggests that the environments removed during refinement can indeed lead to real counter-examples violating ${R}$.

For $X_{02}$, DaRePC is able to find a set of states $X_{c}\subseteq X_{02}$ and $E_{c}\subseteq E_{0}$ such that $\langle{\hat{h}},x_{c},e_{c}\rangle\not\models{R}$. $X_{c}$ and $E_{c}$ are found by calling RefineState on $X_{0}$ 5 times and ShrinkEnv on $E_{0}$ 8 times. The computed set of environmental parameters $E_{c}$ and $X_{c}$ is shown in Fig. 3. We perform 30 simulations starting from randomly sampled $x_{c}\in X_{c}$ under $e_{c}\in E_{c}$ and the results are shown in Fig. 3. We can see clearly from the plot that all the simulation trajectories violates ${R}$, which provides evidence that $X_{c}$ and $E_{c}$ we found are indeed counter-examples.

As we reduce the range of environmental parameters with 0, 3 and 6 refinements, the training data set reduced from 80000 to 71215 and 62638, respectively. Therefore, according to Proposition 2, the empirical conformance measure should at least be $85.8\%$ for all these three cases to achieve the $85\%$ actual conformance measure. In practice, we are able to get $85.9\%$, $87.5\%$ and $89.1\%$ empirical conformance measure. From this, we can see refinement preserves conformance measure of perception contract.

A standard 12-dimensional nonlinear model for the drone is used [12]. The input to the aircraft are the desired roll, pitch, yaw angles, and the vertical thrust. The path for passing through the gates is generated by a planner and the controller tries to follow this planned path. More details about the controller and the dynamics are provided in the Appendix 0.H.

The observations $\langle\hat{x},\hat{y},\hat{z},\hat{\psi}\rangle$ are computed using a particle filter algorithm from [17]. This is a very different perception pipeline compared to ${\sf AutoLand}$. The probability distribution over the state is represented using a set of particles, from which the mean estimate is calculated. Roughly, the particle filter updates the particles in two steps: in the prediction step it uses the dynamics model to move the particles forward in time, and in the correction step it re-samples the particles to select those particles that are consistent with the actual measurement (images in this case). The details of this algorithm are not important for our analysis. However, it is important to note that the particles used for prediction and correction do not have access to the environment parameters (e.g. lighting).

Besides using current image, the particle filter also uses history information to help estimation and therefore the estimation accuracy may improve over time. The shape of the reference trajectory that the drone is following can also influence its the performance, especially rapid turning in the reference trajectory. Therefore, consider this specific application, we decided to sample data along the reference trajectory for constructing the perception contract which gives similar distribution when the drone is following the reference trajectory.

We study the impact of two environmental parameters: (1) Fog ranging from $0$ (clear) to $1$ (heavy fog), and (2) Ambient light ranging from $-1$ (dark) and 0 (bright). The nominal environment $e_{d}=\langle 0,0\rangle$ is a scenario in which the drone is able to complete the path successfully. The effect of different environments on the same view are shown in Fig. 1.

For $X_{0}$, with 23 refinements on the environmental, DaRePC is able to show that $X_{0}$ is safe. The environment set $\tilde{E}$ that was proved safe is ball-like region around nominal environment $e_{d}=\langle 0,0\rangle$. The empirical conformance measure of the contract is $72.4\%$, which is higher than the minimal empirical conformance needed to get the desired conformance with confidence $\delta$. The computed $\textsc{Reach}(X_{0},M_{\tilde{E}},t)$ reachable set ${R}$ shows correctness with respect to the requirement ${R}$ (Fig. 5), that is, $\langle{M}_{\tilde{E}},X_{0},\tilde{E}\rangle\models{R}$.

We run 20 random simulated trajectories starting from randomly sampled $x\in X_{0}$ and $e\in\tilde{E}$. The results are visualized by the blue trajectories in Fig. 5. We can see all the 20 simulations are covered by the Reach computed and therefore doesn’t violate ${R}$. This provides evidence that the $\langle{\hat{h}},X_{0},\tilde{E}\rangle\models{R}$. We also measure the empirical conformance measure of the perception contract for states in these 20 random simulations and the contract is able to get $93.6\%$ empirical conformance measure on these states.

We run 20 additional simulations starting from randomly sampled $x\in X_{0}$ under environments randomly sampled from outside of $\tilde{E}$. The results are shown in Fig. 7 in appendix. We observe that among all 20 simulations, the drone violates requirments in 19 simulations. This provides evidence that the system can easily violate the requirement outside the environmental factors $\tilde{E}$ DaRePC identified.