text:
\section{Theorems and Proofs}

\begin{thm}[\textbf{Runtime Assurance}]
For a well-formed \textsc{RTA}\xspace module $M$, let ${\phi_{\mathtt{Inv}}}(\texttt{mode},{s})$ denote the predicate $(\texttt{mode=SC} \wedge {s}\in\phi_{safe}) \vee (\texttt{mode=AC} \wedge \ensuremath{Reach}_{M}({s}, *,\ensuremath{\Delta})\subseteq\phi_{safe})$.
If the initial state satisfies the invariant ${\phi_{\mathtt{Inv}}}$,
then every state ${s}_t$ reachable from ${s}$ will also satisfy the invariant
${\phi_{\mathtt{Inv}}}$.
	\label{thm:apprta}
\end{thm}
\begin{proof}
	Let $(\texttt{mode},{s})$ be the initial mode and initial state of the system.
	We are given that the invariant holds at this state.
	Since the initial mode is {\sc SC}\xspace,  then, by assumption, ${s}\in\phi_{safe}$.
	We need to prove that all states ${s}_t$ reachable from ${s}$ also satisfy the invariant.
	If there is no mode change, then invariance is satisfied by Property~\cond{P2a}.
	Hence, assume there are mode switches.
	We prove that in every time interval between two consecutive executions of the {\sc DM}\xspace, the invariant holds.
	So, consider time $T$ when the {\sc DM}\xspace executes.
	\\
	(Case1)
	The mode at time $T$ is {\sc SC}\xspace and there is no mode switch at this time.
	Property \cond{P2a} implies that all future states will satisfy the invariant.
	\\
	(Case2)
	The mode at time $T$ is {\sc SC}\xspace and there is a mode switch to {\sc AC}\xspace at this time.

	Then, the current state ${s}_T$ at time $T$ satisfies the condition ${s}_T\in\phi_{safer}$.
	By Property~\cond{P3}, we know that $\ensuremath{Reach}_{M}({s}_T,*,2\Delta) \subseteq \phi_{safe}$, and hence,
	it follows that
	$\ensuremath{Reach}_{M}({s}_T,*,\Delta) \subseteq \phi_{safe}$, and hence the invariant ${\phi_{\mathtt{Inv}}}$ holds at time $T$.
	In fact, irrespective of what actions {\sc AC}\xspace\ applies to the plant, Property~\cond{P3} guarantees that
	the invariant will hold for the interval $[T,T+\ensuremath{\Delta}]$.
	Now, it follows from Property~\cond{P1} that the {\sc DM}\xspace\ will execute again at or before
	the time instant $T+\ensuremath{\Delta}$, and hence the invariant holds until the next execution of {\sc DM}\xspace.
	\\
	(Case3)
	The current mode at time $T$ is {\sc AC}\xspace and there is a mode switch to {\sc SC}\xspace at this time.
	Then, the current state ${s}_T$ at time $T$ satisfies the condition
	$\ensuremath{Reach}_{M}({s}_T,*,2\ensuremath{\Delta})\not\subseteq\phi_{safe}$.
	Since the mode at time $T-\epsilon$ was still {\sc AC}\xspace, and by inductive hypothesis we know that the
	invariant held at that time; therefore,
	we know that $\ensuremath{Reach}_{M}({s}_{T-\epsilon}, *,\ensuremath{\Delta})\subseteq\phi_{safe}$. Therefore,
	for the period $[T-\epsilon,T-\epsilon+\ensuremath{\Delta}]$, we know that the reached state will be in
	$\phi_{safe}$ and the invariant holds.
	Moreover, {\sc SC}\xspace will get a chance to execute in this interval at least once, and
	hence, from that time point onwards, Property~\cond{P2a} will guarantee that the invariant holds.
	\\
	(Case4)
	The current mode at time $T$ is {\sc AC}\xspace and there is a no mode switch.
	Since there is no mode switch at $T$, it implies that
	$\ensuremath{Reach}_{M}({s}_T,*,2\ensuremath{\Delta}) \subseteq \phi_{safe}$ and hence for the next $\ensuremath{\Delta}$ time units,
	we are guaranteed that
	$\ensuremath{Reach}_{M}({s}_T,*,\ensuremath{\Delta}) \subseteq \phi_{safe}$ holds.
\end{proof}

\begin{thm}[Compositional \textsc{RTA}\xspace]
	Let $S = \{M_0, \dots M_n\}$ be an \textsc{RTA}\xspace system. If for all $i$, $M_i$ is a well-formed \textsc{RTA}\xspace module satisfying the safety invariant $\phi^i_{Inv}$ (Theorem~\ref{thm:apprta}) then, the \textsc{RTA}\xspace system $S$ satisfies the invariant $\bigwedge_i \phi^i_{Inv}$.
\end{thm}
\begin{proof}
Note that this theorem simply follows from the fact that composition just restricts the environment.
Since we are guaranteed output disjointness during composition, composition of two modules is guaranteed to be language intersection.
The proof for such composition theorem is described in details in ~\cite{alur1999reactive,lynch1988introduction}.
\end{proof}
\section{Evaluation}
\input{mountaincar_results}
\input{safe_exp_results}
\subsection{Complex safety specifications}
We implemented the above \textsc{RTA}\xspace module described in \shromona{insert section reference} for battery safety when the quadcopter has to travel to multiple goal locations in a given known environment. The results are shown in~\cref{Fig:battery}
\begin{wrapfigure}{l}{0.5\columnwidth}
\centering
\includegraphics[scale=0.3]{figures/battery}
\caption{Navigation with safety constraints on battery}
\label{Fig:battery}
\end{wrapfigure}
In~\cref{Fig:battery}, the grey rectangles, green circles and yellow square represents obstacles, goal locations and battery charging point respectively.

The {\sc DM}\xspace monitors the battery level and planned trajectories of the quadcopter; and when it notices the quadcopter does not have sufficient battery to cover the trajectory hands control to $f_{SC}$. The $f_{SC}$ then plans and executes the quickest trajectory to the battery charging station. Once the battery is charged sufficiently ($> 90\%$), the {\sc DM}\xspace hands control back to the $f_{AC}$ and it can continue to execute the tasks.
\subsection{Battery Safety}

\label{sec:batteryexample}
In this section, we describe how we can use our \textsc{RTA}\xspace module for complex safety specifications coupling the robot high-level mission and its battery level.
A robot can safely navigate in the real world, provided it has sufficient battery.
Battery charge is often not explicitly considered while designing a motion planner that optimizes for completing a specific task.
Optimizing with  battery cost makes the problem harder. Hence, it would be beneficial to decouple these problems and take a more modular approach.

We would like our motion planner to provide battery-safety guarantee, that prioritizes charging the battery when it reaches below a threshold level.
To this effect, we use \textsc{RTA}\xspace based modular approach where the motion planner is optimized for the underlying task, while the \textsc{RTA}\xspace module guarantees battery-safety.

Let $T$ be the maximum battery charge required to go from any point in $\mathcal{W}$ to the battery charging point
and $b_t$ be the current battery charge. We augment the state space of the drone with $b_t$
The components of \textsc{RTA}\xspace are:
$f_{AC}$ can be any motion planner; $f_{SC}$ is designed as a safe motion planner that takes the robot from its current position to the charging point; $\phi_{safe}$ asserts that $b_t > T$; $\phi_{safer}$ asserts that $b_t > 95\%$.
We can define, $\mathtt{ttf}$ as:
$ \mathtt{ttf}(b_t) = \min_t s.t.\ \ensuremath{Reach}(b_t, *, t) \notin \phi_{safe}$.
The resultant \textsc{RTA}\xspace module is well formed and satisfies battery safety properties.

Note that by wrapping the motion planner inside an \textsc{RTA}\xspace module that guarantees battery safety, the entire software stack satisfies the battery safety property irrespective of the application or motion planner used. The video corresponding to this experiment is available at~\url{https://drona-org.github.io/Drona/}

\section{Case Study: Autonomous Mobile Robotics System}

Our canonical application domain for the \text{\small \textsc{Soter}}\xspace runtime assurance framework is safe autonomous mobile robotics systems.
In this section, we provide an overview of the robotics software stack implemented using \text{\small \textsc{Soter}}\xspace and present the terminologies, definitions needed for the rest of the paper.

\subsection{Terminology and Definitions}

\noindent
\textbf{\textit{Workspace:}}
We represent the workspace for a robot $\mathcal{W} \subseteq \mathbb{R}^3$ as a 3-D occupancy map with obstacles (Figure~\ref{fig:tubeexp}).

\noindent
\textbf{\textit{Motion primitives:}}
Motion primitives are a set of short closed-loop trajectories of a robot under the action of a set of precomputed control laws~\cite{planning_book,MellingerK11}.
The set of motion primitives form the basis of the motion of a robot.
The low-level controllers can be used to move the robot from one location to another by continuously changing thrust.
Let $\mathcal{U}$ be the set of low-level controls (e.g. torque) that can be applied to the robot.
For example, we leverage these low-level controllers to implement a motion primitive, $\mathtt{goto}$, that moves the robot from its current location to the goal location along a straight line joining the locations.
We use $\mathbf{x}_t$ to represent $\mathbf{x}(t)$, the current location of the robot.
The $\mathtt{goto}$ motion primitive takes as input the destination position, $\mathbf{x}_{f}$, and generates a sequence of low level controls, $u \in \mathcal{U}$, to take the robot from $\mathbf{x}_{t}$ to $\mathbf{x}_{f}$.

\noindent
\textbf{\textit{Trajectory:}}
The trajectory $\xi$ of a robot under the influence of a motion primitive is a sequence of locations i.e., $\xi = \mathbf{x}_t, \mathbf{x}_{t+1}, \mathbf{x}_{t+2}, \dots$ such that it satisfies the underlying dynamics in Equation~\ref{eqn:sys}.

Let $\dist{\mathbf{x}}{(\mathbf{q}_i,\mathbf{q}_g)}$ be the distance between location $\mathbf{x}_t$ and the line passing through locations $\mathbf{q}_i$ and $\mathbf{q}_g$.

\noindent
\textbf{\textit{$\epsilon$-tube:}}
A robot is within the $\epsilon$-tube surrounding the line passing through points $\mathbf{q}_i$ and $\mathbf{q}_g$, represented by $\tube{(\mathbf{q}_i,\mathbf{q}_g)}{\epsilon}$, if the distance between its current position and the line is bounded by $\epsilon$, i.e.,
$\tube{(\mathbf{q}_i,\mathbf{q}_g)}{\epsilon} := \{ \mathbf{x} \mid \dist{\mathbf{x}}{(\mathbf{q}_i,\mathbf{q}_g)} < \epsilon \}$.

\noindent
\textbf{\textit{Motion plan:}}
A robot moves from its current location to a destination location by executing a motion plan which is a sequence of motion primitives. For example, for a way-point based motion planner using $\mathtt{goto}$ motion primitive, a motion plan $\mu = \mathtt{goto}(\mathbf{x}_1)\dots\mathtt{goto}(\mathbf{x}_g)$ is a sequence of $\mathtt{goto}$'s that drives the robot from its current location to destination location $\mathbf{x}_g$.

\subsection{Overview of the Robotics Software Stack}

\subsection{Correctness of an \textsc{RTA}\xspace System}

\section{Conclusion and Future Directions}

In this paper, we have presented \text{\small \textsc{Soter}}\xspace, a new run-time assurance (\textsc{RTA}\xspace) framework
for programming safe robotics systems.
In contrast with other \textsc{RTA}\xspace frameworks, \text{\small \textsc{Soter}}\xspace provides
(1) a programming
language for modular implementation of safe robotics systems by
combining each advanced controller with a safe counterpart;
(2) theoretical results showing how to safely switch
between advanced and safe controllers, and
(3) experimental results
demonstrating \text{\small \textsc{Soter}}\xspace on drone platforms in both simulation and in
hardware.

Combining multiple \textsc{RTA}\xspace modules that have coordinated (DM) switching is non-trivial.
A system may have multiple components with different guarantees. Our philosophy in this paper is that each component must then use an \textsc{RTA}\xspace instance to assure its guarantees, as this decomposition can help in building complex systems.
Let's consider a system consisting of two \textsc{RTA}\xspace modules M1 and M2, when M1 switches modes (AC to SC), it may require M2 to switch as well so that it can use the guarantee that M2's new controller (SC) provides. This kind of coordinated switching complicates the overall architecture but is an interesting future work.
We also plan to extend the experimental evaluation for
a broader class of robotics platforms (e.g., multi-robot systems), safety specifications (e.g., probabilistic properties), and unknown environments (e.g., dynamic obstacles).
Altogether, such extensions will enable us to make further progress
towards the goal of verified intelligent autonomous systems~\cite{seshia-arxiv16}.

\section*{Acknowledgments}
We sincerely thank the anonymous reviewers and our shepherd Mohamed Kaaniche for their thoughtful comments.
We also thank Daniel Fremont for his valuable feedback and suggested improvements on the previous drafts of the paper.
This work was supported in part by the TerraSwarm Research Center, one of six centers
supported by the STARnet phase of the Focus Center Research Program (FCRP) a Semiconductor
Research Corporation program sponsored by MARCO and DARPA, by the DARPA BRASS and
Assured Autonomy programs, by NSF grants 1545126 (VeHICaL), 1739816, and 1837132,
by Berkeley Deep Drive, and by Toyota under the iCyPhy center.

\section{Evaluation}
\label{sec:eval}

We empirically evaluate the \text{\small \textsc{Soter}}\xspace framework by building an \textsc{RTA}\xspace-protected software stack (Figure~\ref{fig:rtasoftwarestack}) that satisfies the safety invariant: $\phi_{plan}\wedge\phi_{mpr}\wedge\phi_{bat}$.
The goal of our evaluation is twofold:
\cond{Goal1} Demonstrate how the \text{\small \textsc{Soter}}\xspace programming framework can be used for building the software stack compositionally, where each component is guaranteed to satisfy the component-level safety specification. Further, we show how the programmable switching feature of an \textsc{RTA}\xspace module can help maximize its performance.
\cond{Goal2} Empirically validate using rigorous simulations that an \textsc{RTA}\xspace-protected software stack can ensure the safety of the drone in the presence of third-party (or machine learning) components, where otherwise, the drone could have crashed.

\textit{The videos and other details corresponding to our experiments on real drones are available on {\color{blue} \url{https://drona-org.github.io/Drona/}}.}

\noindent
\textbf{\text{\small \textsc{Soter}}\xspace tool chain.}
The \text{\small \textsc{Soter}}\xspace tool-chain consists of three components: the compiler, a C runtime and a backend systematic testing engine.
The compiler first checks that all the constructed \textsc{RTA}\xspace modules in the program are well-formed.
The compiler then converts the source-level syntax of a \text{\small \textsc{Soter}}\xspace program into C code.
This code contains statically-defined C array-of-structs and functions for
the topics, nodes, and functions declarations.
The $\ensuremath{OE}$ that controls the output of each node is implemented as a shared-global data-structure updated by all the {\sc DM}\xspace in the program.
The \text{\small \textsc{Soter}}\xspace C runtime executes the program according to the program's operational semantics by using the C representation of the nodes.
The periodic behavior of each node was implemented using OS timers for our experiments, deploying the generated code on real-time operating system is future work.

The compiler also generates C code that can be systematically explored by the backend testing engine.
This part of the \text{\small \textsc{Soter}}\xspace framework is built on top of our previous work~\cite{DesaiQS18} on the \textsc{P}\xspace~\cite{pasync,oopsla2018} language and the {\sc Drona}~\cite{Desai:2017} robotics framework.
The systematic testing engine enumerates, in a model-checking style,
all possible executions of the program by controlling the interleaving of nodes using an external scheduler.
Since a \text{\small \textsc{Soter}}\xspace program is a multi-rate periodic system, we use a bounded-asynchronous scheduler~\cite{fisher2008bounded} to explore only those schedules that satisfy the bounded-asynchrony semantics.
When performing systematic testing of the robotics software stack the third-party (untrusted) components that are not implemented in \text{\small \textsc{Soter}}\xspace are replaced by their abstractions implemented in \text{\small \textsc{Soter}}\xspace.
The systematic testing backend details is not provided as the focus of our paper is to demonstrate the importance of runtime assurance after design-time analysis.

\noindent
\textit{\textbf{Experimental Setup}}
For our experiments on the real drone hardware, we use a 3DR Iris~\cite{3dr} drone that comes with the open-source Pixhawk PX4~\cite{px4} autopilot.
The simulation results were done in the Gazebo~\cite{koenig2004design} simulator environment that has high fidelity models of Iris drone.
For our simulations, we execute the PX4 firmware in the loop.

\input{tube_results}

\subsection{\textsc{RTA}\xspace-Protected Battery Safety}
We want our software stack to provide the battery-safety guarantee, that prioritizes safely landing the drone when the battery charge falls below a threshold level.

We first augment the state of the drone with the current battery charge, $b_t$.
$\ensuremath{N_{ac}}$  is a node that receives the current motion plan from the planner and simply forwards it to the motion primitives module.
$\ensuremath{N_{sc}}$ is a certified planner that safely lands the drone from its current position.
The set of all safe states for the battery safety is given by, $\phi_{safe} := b_t > 0$, i.e., the drone is safe as long as the battery does not run out of charge. We define $\phi_{safer} := b_t > 85\%$, i.e., the battery charge is greater than $85\%$.
Since the battery discharges at a slower rate compared to changes in the position of the drone, we define a larger $\ensuremath{\Delta}$ for the battery \textsc{RTA}\xspace compared to the motion primitive \textsc{RTA}\xspace.

To design the $\mathtt{ttf}_{2\ensuremath{\Delta}}$, we first define two terms: (1) Maximum battery charge required to land $T_{max}$; and (2) Maximum battery discharge in $2\ensuremath{\Delta}$, $cost^*$.
In general $T_{max}$ depends on the current position of the drone. However, we approximate $T_{max}$ as the battery required to land from the maximum height attained by the drone safely.
Although conservative, it is easy to compute and can be done offline.
To find $cost^*$, we first define a function $cost$, which given the low-level control to the drone and a time period, returns the amount of battery the drone discharges by applying that control for the given time period. Then, $cost^* = \max_{u} cost(u, 2 \ensuremath{\Delta})$ is the maximum discharge that occurs in time $2 \ensuremath{\Delta}$ across all possible controls, $u$.
We can now define $\mathtt{ttf}_{2\ensuremath{\Delta}}(b_t, \phi_{safe}) = b_t - cost^* < T_{max}$.
It guarantees that DM switches control to SC if the current battery level may not be sufficient to safely land if AC were to apply the worst possible control.
{\sc DM}\xspace returns control to $\ensuremath{N_{ac}}$ once the drone is sufficiently charged. This is defined by $\phi_{safer}$, which is chosen to assert that the battery has at least $85\%$ charge before {\sc DM}\xspace can hand control back to AC.
The resultant \textsc{RTA}\xspace module is well-formed and satisfies the battery safety property $\phi_{bat}$.
We implemented the battery safety \textsc{RTA}\xspace module with the components defined above. Figure~\ref{fig:results}c shows a trajectory, where the battery falls below the safety threshold causing DM to transfer control to $\ensuremath{N_{sc}}$ which lands the drone.

\subsection{\textsc{RTA}\xspace for Safe Motion Planner}
\label{ssec:plan}
We use OMPL~\cite{ompl}, a third-party motion-planning library that implements many state-of-the-art sampling-based motion planning algorithms.
We implemented the motion-planner for our surveillance application using the RRT*~\cite{karaman2011sampling} algorithm from OMPL.
We injected bugs into the implementation of RRT* such that in some cases the generated motion plan can collide with obstacles.
We wrapped the motion-planner inside an \textsc{RTA}\xspace module to ensure that the waypoints generated by motion plan do not collide with an obstacle (violating $\phi_{plan}$).

To summarize, we used the theory of well-formed \textsc{RTA}\xspace module to construct three \textsc{RTA}\xspace modules: motion primitives, battery safety, and motion planner.
We leverage Theorem~\ref{thm:rta} to ensure that the modules individually satisfy the safety invariants $\phi_{mpr}$, $\phi_{bat}$, and $\phi_{plan}$ respectively.
The \textsc{RTA}\xspace-protected software stack (Figure~\ref{fig:casestudy}c) is a composition of the three modules and using Theorem~\ref{thm:comp} we can guarantee that the system satisfies the desired safety invariant $\phi_{plan} \wedge \phi_{mpr} \wedge \phi_{bat}$.

\subsection{Rigorous Simulation}
To demonstrate that \text{\small \textsc{Soter}}\xspace helps build robust robotics systems we conducted rigorous stress testing of the \textsc{RTA}\xspace-protected drone software stack.
We conducted software in the loop simulations for 104 hours, where an autonomous drone is tasked to visit randomly generated surveillance points in the Gazebo workspace repeatedly (Figure~\ref{fig:casestudy}). In total, the drone flew for approximately 1505K meters in the 104 hours of simulation.
We found that there were 109 disengagements, these are cases where one of the {\sc SC}\xspace nodes took control from {\sc AC}\xspace and avoided a potential failure.
There were 34 crashes during the experiments, and we found that in all these cases the problem was that the {\sc DM}\xspace node did switch control, but the {\sc SC}\xspace node was not scheduled in time for the system to recover.
We believe that these crashes can also be avoided by running the software stack on a real-time operating system.
We also found that as the \textsc{RTA}\xspace module is designed to return the control to {\sc AC}\xspace after recovering the system, during our simulations, {\sc AC}\xspace nodes were in control for $> 96\%$ of the time. Thus, safety is ensured without sacrificing the overall performance.

\section{\text{\small \textsc{Soter}}\xspace Tool Chain}

\label{sec:implementation}

The \text{\small \textsc{Soter}}\xspace tool-chain consists of two components: the compiler and a C runtime.
The compiler converts the source-level syntax of a \text{\small \textsc{Soter}}\xspace program into C code.
This code contains statically-defined C array-of-structs and functions for
the topics, nodes, and functions declarations.
The $\ensuremath{OE}$ that controls the output of each node is implemented as a shared-global data-structure updated by all the ${\sc DM}\xspace$s in the program.
The \text{\small \textsc{Soter}}\xspace C runtime executes the program according to the program's operational semantics by using the C representation of the nodes.
The periodic behavior of each node was implemented using OS timers for our experiments, deploying the generated code on real-time operating system is future work.

\ankush{need to add details about the testing infrastructure}

\section{Introduction}
\label{sec:intro}

Robotic systems are increasingly playing diverse and safety-critical roles in society, including delivery systems,
surveillance, and personal transportation. This drive towards autonomy is also leading to ever-increasing levels of software complexity,
including integration of advanced data-driven, machine-learning components.
This complexity comes on top of the existing challenge of designing
safe event-driven, real-time, concurrent software required for
robotics applications.
However, advances in formal verification and systematic testing have yet to catch up with this increased complexity~\cite{seshia-arxiv16}.
Moreover, the dependence of robotic systems on third-party off-the-shelf components and machine-learning techniques is predicted to increase.
This has resulted in a widening gap between the complexity of systems being deployed
and those that can be certified for safety and correctness.

One approach to bridging this gap is to leverage techniques for \textit{run-time assurance}, where the results of design-time verification
are used to build a system that monitors itself and its environment at run time;
and, when needed, switches to a provably-safe operating mode, potentially at
lower performance and sacrificing certain non-critical objectives. A prominent example of
a Run-Time Assurance ($\textsc{RTA}\xspace$) framework is the \textit{Simplex Architecture}~\cite{sha2001using}, which has been used for
building provably-correct safety-critical avionics~\cite{schierman2015runtime,SetoCaseStudy2000},
robotics~\cite{phan2017collision} and cyber-physical systems~\cite{sandboxingcontrollers,clark2013study,pacemaker}.

The typical $\textsc{RTA}\xspace$ architecture based on Simplex~\cite{sha2001using}
(see Figure~\ref{fig:simplexarchitecture})
comprises three sub-components:
\point{1} The \textit{advanced controller} ({\sc AC}\xspace) that controls the robot under nominal operating conditions, and is designed to achieve \textit{high-performance} with respect to specialized metrics (e.g., fuel economy, time), but it is not provably safe,
\point{2} The \textit{safe controller} ({\sc SC}\xspace) that can be pre-certified to keep the robot within a region of safe operation for the plant/robot, usually at the cost of lower performance, and
\point{3} The \textit{decision module} ({\sc DM}\xspace) which is pre-certified (or automatically synthesized to be correct) to periodically monitor the state of the plant and the environment to determine when to switch from {\sc AC}\xspace to {\sc SC}\xspace so that the system is guaranteed to stay within the safe region.
When {\sc AC}\xspace is in control of the system, {\sc DM}\xspace monitors (samples) the system state every $\ensuremath{\Delta}$ period to check whether the system can violate the desired safety specification ($\phi$) in time $\ensuremath{\Delta}$. If so, then {\sc DM}\xspace switches control to {\sc SC}\xspace.

\begin{wrapfigure}{l}{0.57\columnwidth}
	\centering
	\vspace{-0.3cm}
	\includegraphics[scale=0.38]{figures/simplex.png}
	\vspace{-0.55cm}
	\caption{\textsc{RTA}\xspace Architecture}
	\vspace{-0.25cm}
	\label{fig:simplexarchitecture}
\end{wrapfigure}

This Simplex-based \textsc{RTA}\xspace architecture is a very useful high-level framework, but
there are several limitations of its existing instantiations.
First, existing techniques either apply \textsc{RTA}\xspace~\cite{Bohrer2018,phan2017component,schierman2015runtime} to a single untrusted component in the system or wrap the large monolithic system into a single instance of Simplex which makes the design and verification of the corresponding SC and DM difficult or infeasible.
Second, most prior applications of \textsc{RTA}\xspace do not provide high-level {\em programming language support} for constructing provably-safe \textsc{RTA}\xspace systems
in a {\em modular} fashion while designing for {\em timing and communication behavior} of such systems.
In order to ease the construction of \textsc{RTA}\xspace systems, there is a need
for a general programming framework for building provably-safe robotic software systems with run-time assurance
that also considers implementation aspects such as timing and communication.
Finally, existing techniques do not provide a principled and safe way for {\sc DM}\xspace
to switch back from SC to {\sc AC}\xspace so as to keep performance penalties to a minimum
while retaining strong safety guarantees.

In this paper, we seek to address these limitations by developing \text{\small \textsc{Soter}}\xspace,
a programming framework for building safe robotics systems using runtime assurance.
A \text{\small \textsc{Soter}}\xspace program is a collection of periodic processes, termed {\em nodes}, that interact with each other using
a publish-subscribe model of communication (which is popular in robotics, e.g.,
in Robot Operating System, ROS~\cite{ROS}).
An \textsc{RTA}\xspace module in \text{\small \textsc{Soter}}\xspace consists of an advanced controller node, a safe controller node and a safety specification; if the module is well-formed then the framework provides a guarantee that the system satisfies the safety specification.
\text{\small \textsc{Soter}}\xspace allows programmers to declaratively construct an \textsc{RTA}\xspace module with specified timing behavior, combining provably-safe operation with the feature
of using {\sc AC}\xspace whenever safe so as to achieve good performance.
\text{\small \textsc{Soter}}\xspace provides a provably-safe way for {\sc DM}\xspace to switch back from
{\sc SC}\xspace to {\sc AC}\xspace, thus extending the traditional \textsc{RTA}\xspace framework and
providing higher performance.
Our evaluation demonstrates that \text{\small \textsc{Soter}}\xspace is effective at achieving this blend of safety and performance.

Crucially, \text{\small \textsc{Soter}}\xspace supports compositional construction of the overall \textsc{RTA}\xspace system.
The \text{\small \textsc{Soter}}\xspace language includes constructs for decomposing the design
and verification of the overall \textsc{RTA}\xspace system into that for individual \textsc{RTA}\xspace modules while
retaining guarantees of safety for the overall composite system.
\text{\small \textsc{Soter}}\xspace includes a compiler that generates the {\sc DM}\xspace node that implements the switching logic, and which also
generates C code to be executed on common robotics software platforms such as ROS~\cite{ROS} and MavLink~\cite{px4}.

We evaluate the efficacy of the \text{\small \textsc{Soter}}\xspace framework by building a safe autonomous drone surveillance system.
We show that \text{\small \textsc{Soter}}\xspace can be used to build a complex robotics software stack consisting of both third-party untrusted components and complex machine learning modules, and still provide system-wide correctness guarantees.
The generated code for the robotics software has been tested both on an actual drone platform (the 3DR~\cite{3dr} drone) and in simulation (using the ROS/Gazebo~\cite{koenig2004design} and OpenAI Gym~\cite{openai}).
Our results demonstrate that the \textsc{RTA}\xspace-protected software stack built using \text{\small \textsc{Soter}}\xspace can ensure the safety of the drone both when using unsafe third-party controllers and in the presence of bugs introduced using fault injection in the advanced controller.

\noindent
In summary, we make the following novel contributions:
\begin{mylist}
\item A programming framework for a Simplex-based run-time assurance system that provides language primitives for the modular design of safe robotics systems (Sec.~\ref{sec:rta-module});
\item A theoretical formalism based on computing reachable sets that keeps the system provably safe while maintaining smooth switching behavior from advanced to a safe controller {\em and vice-versa} (Sec.~\ref{sec:correctness});
\item A framework for the modular design of run-time assurance (Sec.~\ref{sec:semantics}), and
\item Experimental results in simulation and on real drone platforms demonstrating how \text{\small \textsc{Soter}}\xspace can be used for guaranteeing correctness of a system even in the presence of untrusted or unverified components (Sec.~\ref{sec:eval}).
\end{mylist}

\section{Runtime Assurance Module}
\label{sec:rta-module}

In this section, we formalize the \text{\small \textsc{Soter}}\xspace runtime assurance module and present the well-formedness conditions required for its correctness. We conclude by informally describing the behavior of a system protected by an \textsc{RTA}\xspace module.

\subsection{Programming Model}
Recollect that a program in \text{\small \textsc{Soter}}\xspace is a collection of periodic nodes communicating with each other by publishing on and subscribing to message topics.

\noindent
\textbf{Topic.}
Formally, a topic is a tuple $(e, v)$ consisting of a unique name $\ensuremath{e}\in \ensuremath{\mathcal{T}}$, where $\ensuremath{\mathcal{T}}$ is the  universe of all topic names, and a value $\ensuremath{v}\in\ensuremath{\mathcal{V}}$, where $\ensuremath{\mathcal{V}}$ is the universe of all possible values that can be communicated using topic $\ensuremath{e}$. For simplicity of presentation: (1) we assume that all topics share the
same set $\ensuremath{\mathcal{V}}$ of possible values and (2) instead of modeling the local buffers associated with each subscribed topic of a node; we model the communication between nodes using the global value associated with each topic.

Let $\ensuremath{\mathcal{N}}$ represent the set of names of all the nodes.
We sometimes refer to a node by its unique name, for example, when $\ensuremath{N_{ac}} \in \ensuremath{\mathcal{N}}$ and we say ``node $\ensuremath{N_{ac}}$'', we are referring to a node with name $\ensuremath{N_{ac}}$.
Let $\ensuremath{\mathcal{L}}$ represent the set of all possible values the local state of any node could have during its execution.
A \textit{valuation} of a set $X \subseteq \ensuremath{\mathcal{T}}$ of topic names is a map from each topic name $x \in X$ to the value $v$ stored at topic $(x, v)$.
Let $\Vals{X}$ represent the valuations of set $X$.

\noindent
\textbf{Node.}
A node in \text{\small \textsc{Soter}}\xspace is a tuple $(\ensuremath{N}, \ensuremath{I}, \ensuremath{O}, \ensuremath{T}, \ensuremath{C})$ where:
\begin{mylist}
	\item $\ensuremath{N} \in \ensuremath{\mathcal{N}}$ is the unique name of the node.
	\item $\ensuremath{I} \subseteq \ensuremath{\mathcal{T}}$ is the set of names of all topics subscribed to by the node (inputs).
	\item $\ensuremath{O} \subseteq \ensuremath{\mathcal{T}}$ is the set of names of all topics on which the node publishes (output). The output topics are disjoint from the set of input topics ($\ensuremath{I} \cap \ensuremath{O} = \emptyset$).
	\item $\ensuremath{T} \subseteq \ensuremath{\mathcal{L}} \times (\ensuremath{I} \rightarrow \ensuremath{\mathcal{V}}) \times \ensuremath{\mathcal{L}} \times (\ensuremath{O} \rightarrow \ensuremath{\mathcal{V}})$ is the transition relation of the node.
	If $(\ensuremath{l}, \Vals{\ensuremath{I}}, \ensuremath{l}', \Vals{\ensuremath{O}}) \in \ensuremath{T}$, then on the \textit{input} (subscribed) topics valuation of $\Vals{\ensuremath{I}}$, the local state of the node moves from $\ensuremath{l}$ to $\ensuremath{l}'$ and publishes on the \textit{output} topics to update its valuation to $\Vals{\ensuremath{O}}$.
	\item $\ensuremath{C} = \{(N, t_0), (N, t_1), \dots\}$ is the time-table representing the times $t_0, t_1, \dots$ at which the node $N$ takes a step.
\end{mylist}

Intuitively, a node is a periodic input-output state-transition system: at every time instant
in its calendar, the node reads the values in its input topics, updates its local state, and publishes
values on its output topics.
Note that we are using the timeout-based discrete event simulation~\cite{dutertre2004modeling} to model the periodic real-time process as a standard transition system (more details in Section~\ref{sec:semantics}).
Each node specifies, using a time-table, the fixed times at which it should be scheduled.
For a periodic node with period $\delta$, the calendar will have entries
$(\ensuremath{N},t_0),(\ensuremath{N},t_1),\ldots$ such that $t_{i+1} - t_{i} = \delta$ for all $i$.
We refer to the components of a node with name $N \in \ensuremath{\mathcal{N}}$ as $\Inputs{N}, \Outputs{N}, \Transitions{N}$ and $\Calendar{N}$ respectively. We use $\Period{N}$ to refer to the period $\delta$ of node $N$.

\subsection{Runtime Assurance Module}
Let $\mathcal{S}$ represent the state space of the system, i.e., the set of all possible configurations of the system (formally defined in Section~\ref{sec:semantics}).
We assume that the desired safety property is given in the form of a subset $\phi_{safe} \subseteq \mathcal{S}$ ({\textit{safe states}}).
The goal is to ensure using an \textsc{RTA}\xspace module that the system always stays inside the safe set $\phi_{safe}$.

\noindent
\textbf{\textsc{RTA}\xspace Module.}
An \textsc{RTA}\xspace module is represented as a tuple $(\ensuremath{N_{ac}}, \ensuremath{N_{sc}}, \ensuremath{N_{dm}}, \ensuremath{\Delta}, \phi_{safe}, \phi_{safer})$ where:
\begin{mylist}
	\item $\ensuremath{N_{ac}} \in \ensuremath{\mathcal{N}}$ is the advanced controller ({\sc AC}\xspace) node,
	\item $\ensuremath{N_{sc}} \in \ensuremath{\mathcal{N}}$ is the safe controller ({\sc SC}\xspace) node,
	\item $\ensuremath{N_{dm}} \in \ensuremath{\mathcal{N}}$ is the decision module ({\sc DM}\xspace) node,
	\item $\ensuremath{\Delta} \in \mathbb{R}^+$ represents the period of {\sc DM}\xspace ($\delta(\ensuremath{N_{sc}}) = \Delta$),
	\item $\phi_{safe} \subseteq \mathcal{S} $ is the desired safety property.
	\item $\phi_{safer} \subseteq \phi_{safe}$ is a stronger safety property.
\end{mylist}

\begin{figure}[h]
	\centering
	\vspace{-0.2cm}
	\includegraphics[scale=0.42]{code/dm.png}
	\vspace{-0.7cm}
	\caption{Decision Module Switching Logic for Module M}
	\vspace{-0.1cm}
	\label{fig:dmlogic}
\end{figure}

Given an $\textsc{RTA}\xspace$ module $M$, Figure~\ref{fig:dmlogic} presents the switching logic that sets the
{\em{mode}} of the \textsc{RTA}\xspace module given the current state $s_t$ of the system.
The {\sc DM}\xspace node evaluates this switching logic once every $\ensuremath{\Delta}$ time unit.
When it runs, it first reads the current state $s_t$ and sets $mode$ based on it.
Note that the set $\phi_{safer}$ determines when it is safe to switch from $\ensuremath{N_{sc}}$ to $\ensuremath{N_{ac}}$.
$\ensuremath{Reach}_{M}({s}, *, t) \subseteq \mathcal{S}$ represents the set of all states reachable in time $[0,t]$ starting from the state ${s}$, using
{\em any non-deterministic controller}. We formally define $\ensuremath{Reach}$ in Section~\ref{sec:semantics}, informally, $\ensuremath{Reach}_{M}(s_t,*,2\ensuremath{\Delta}) \not\subseteq\phi_{safe}$ checks that the system will remain inside $\phi_{safe}$ in the next $2\ensuremath{\Delta}$ time.
This $2\ensuremath{\Delta}$ look ahead is used to determine when it is necessary to switch to using $\ensuremath{N_{sc}}$, in order to ensure that the $\ensuremath{N_{sc}}$ ($\Period{\ensuremath{N_{sc}}} \leq \Delta$) will be executed at least once before the system leaves $\phi_{safe}$.
The \text{\small \textsc{Soter}}\xspace compiler automatically generates a unique {\sc DM}\xspace node ($\ensuremath{N_{dm}}$) for each primitive \textsc{RTA}\xspace module declaration.

For an \textsc{RTA}\xspace module $(\ensuremath{N_{ac}}, \ensuremath{N_{sc}}, \ensuremath{N_{dm}}, \ensuremath{\Delta}, \phi_{safe}, \phi_{safer})$, {\sc DM}\xspace is the node $(\ensuremath{N_{dm}}, \ensuremath{I}_{dm}, \emptyset, \ensuremath{T}_{dm}, \ensuremath{C}_{dm})$ where:
\begin{mylist}
	\item The local state is a binary variable \textit{mode} : $\{{\sc AC}\xspace, {\sc SC}\xspace\}$.
	\item Topics subscribed by {\sc DM}\xspace include the topics subscribed by either of the nodes; i.e.,
	$\Inputs{\ensuremath{N_{ac}}} \subseteq \ensuremath{I}_{dm}$ and $\Inputs{\ensuremath{N_{sc}}} \subseteq \ensuremath{I}_{dm}$.
	\item {\sc DM}\xspace does not publish on any topic. But it updates a global data structure that controls the outputs of {\sc AC}\xspace and {\sc SC}\xspace nodes (more details in Section~\ref{sec:semantics}).
	\item If $(mode, \Vals{\ensuremath{I}_{dm}}, mode',\emptyset) \in \ensuremath{T}_{dm}$, then the local state moves from $mode$ to $mode'$ based on the logic in Figure~\ref{fig:dmlogic}.
	\item $\ensuremath{C}_{dm} = \{ (\ensuremath{N_{dm}}, t_0), (\ensuremath{N_{dm}}, t_1), \dots\}$ where $\forall_i | t_i - t_{i+1} | = \Delta$ represents the time-table of the node.
\end{mylist}

We are implicitly assuming that the topics $\ensuremath{I}_{dm}$ read by the {\sc DM}\xspace contain enough information to
evaluate $\phi_{safe}$, $\phi_{safer}$, and perform the reachability computation described in Section~\ref{sec:semantics}.
Given a declaration of the \textsc{RTA}\xspace module (Figure~\ref{fig:rtamodule}), the \text{\small \textsc{Soter}}\xspace compiler can automatically generate its {\sc DM}\xspace.

\subsection{Runtime Assurance for Machine Learning Components}

Use of machine learning techniques for designing controllers and policies in robotics is increasing as these systems grow in complexity and operate in uncertain environments.
Specifically, Reinforcement learning~\cite{kaelbling1996reinforcement} (RL) is being used intensively for synthesizing controllers for robotic systems. In RL, an agent learns a controller or policy by interacting with its environment and receiving a rewards for its action.
However, the policy learned depends heavily on the scenarios the agent has seen, and generalization to new environments can be erroneous.
Ideally the system uses the machine learned modules under nominal conditions but switches to a safe component when the output of the learned module cannot be trusted. This can be captured by \textsc{RTA}\xspace module.

\begin{wrapfigure}{l}{0.6\columnwidth}
	\centering
	\includegraphics[scale=0.2]{figures/mountaincar.png}
	\caption{Mountain-car environment with cliff}
	\label{Fig:mountaincar}
\end{wrapfigure}

For our case study, we use a popular OpenAI Gym~\cite{openai} example of a Mountain-car.
In the mountain-car example (Figure~\ref{Fig:mountaincar}), a car is on a one-dimensional track, positioned between two mountains.
The goal is to drive up the mountain on the right to the flag; however, the car's engine is not strong enough to scale the mountain in a single pass.
Therefore, the only way to succeed is to drive back and forth to build up momentum.
Moreover, we modify the original scenario to include a cliff on the left, which the mountain-car must avoid at all costs.
The configuration of the system is a pair $\mathbf{x}_t = (x_t, v_t)$ where $p_t$ is the current position and $v_t$ is the current velocity of the car; and the input control is the acceleration, $u = a_t$.

To design the \textsc{RTA}\xspace module, we need to (1) Design the components of the \textsc{RTA}\xspace module $\ensuremath{N_{ac}}$, $\ensuremath{N_{sc}}$, $\ensuremath{\Delta}$, $\phi_{safe}$ and $\phi_{safer}$; and (2) Design the switching logic from AC to SC and from SC to AC.

\textbf{\textit{Designing the \textsc{RTA}\xspace components.}} $\ensuremath{N_{ac}}$ in this case is a state based controller trained using reinforcement learning. $\ensuremath{N_{sc}}$ and $\phi_{safe}$ can be computed using the level set tool box~\cite{reachability}. We compute the backward reachable set from the goal by treating the cliff as an obstacle, which returns the set of all states which can ultimately reach the goal without falling of the cliff. This set is our $\phi_{safe}$. Our $\ensuremath{N_{sc}}$ is the safe optimal controller returned by the level set toolbox. In our experiments we choose $\phi_{safer} = \SR{\phi_{safe}}{2 \ensuremath{\Delta}}$ and $\ensuremath{\Delta} = \Period(\ensuremath{N_{sc}})  = \Period(\ensuremath{N_{ac}})$.

\textbf{\textit{Designing switching logic.}} In this experiment, we define the switching condition from AC to SC with the boolean function $\mathtt{ttf}_{2 \ensuremath{\Delta}}(\mathbf{x}_t, \phi_{safe}) = \mathbf{x}_t \notin \SR{\phi_{safe}}{2 \ensuremath{\Delta}}$ which is true for all states which can leave $\phi_{safe}$ in $2 \ensuremath{\Delta}$ time. In this example this ends up being states in $\phi_{safe}$ which are outside $\phi_{safer}$. For switching from SC to AC, we choose the boundary of $\SR{\phi_{safer}}{\ensuremath{\Delta}} \subset \phi_{safer}$.

\textbf{\textit{Experimental results.}} Figure~\ref{Fig:safe_control} shows an unsafe behavior (blue trajectory) of the learned controller where the trajectory starting at $s_0$ enters the unsafe region (shown in gray), which is the set of position and velocities which lead to the car falling off the cliff.

\begin{wrapfigure}{l}{0.6\columnwidth}
	\includegraphics[scale=0.3]{figures/safe_control.png}
	\caption{\textsc{RTA}\xspace protected safe mountain-car}
	\label{Fig:safe_control}
\end{wrapfigure}
$\phi_{safe}$ is the region shown in light orange, and $\SR{\phi_{safer}}{\ensuremath{\Delta}}$ is shown in green.
The system is designed such that $\ensuremath{\Delta} = 1$ and it satisfies all the well-formedness constrains for the \textsc{RTA}\xspace module.
The resulting \textsc{RTA}\xspace module produces the trajectory shown in blue ($\ensuremath{N_{ac}}$ in control), green ($\ensuremath{N_{sc}}$ in control) and blue ($\ensuremath{N_{ac}}$ back in control) with the switching points shown as purple dots.
The resultant system is always able to drive the trajectory to the goal $g$, the advanced controller is used most part of the trajectory (blue), except for safe controller being used when the car is too close to the cliff.

\section{Overview}
We illustrate the \text{\small \textsc{Soter}}\xspace framework for programming safe robotics systems by using our case study of an autonomous drone surveillance system.

\subsection{Case Study: Drone Surveillance System}
\label{sec:softwarestack}
In this paper, we consider the problem of building a surveillance system where an autonomous drone must safely patrol a city.
Figure~\ref{fig:casestudy} (left) presents a snapshot of the city workspace from the ROS/Gazebo simulator~\cite{koenig2004design} and
Figure~\ref{fig:casestudy} (right) presents the corresponding obstacle map.

\begin{figure}
	\centering

	\includegraphics[scale=0.36]{figures/combmap.png}
	\caption{Case Study: A Drone Surveillance System}
	\vspace{-0.2cm}
	\label{fig:casestudy}
\end{figure}
For our case study, we consider a simplified setting where all the obstacles (houses, cars, etc.) are static, known a priori, and that there are no environment uncertainties like wind.
Even for such a simplified setup the software stack (Figure~\ref{fig:softwarestack}) is complex: consisting of multiple components interacting with each other and uses uncertified components (red blocks).

\noindent
\textbf{Drone software stack.}
The application layer implements the surveillance protocol that ensures the application specific property, e.g., all surveillance points must be visited infinitely often.
The generic components of the software stack consists of the motion planner and the motion primitives.

\begin{wrapfigure}{l}{0.5\columnwidth}
	\centering
	\vspace{-0.3cm}
	\includegraphics[scale=0.35]{figures/softwarestack.png}
	\vspace{-0.5cm}
	\caption{{\small Drone Software Stack}}
	\vspace{-0.2cm}
	\label{fig:softwarestack}
\end{wrapfigure}

For surveillance, the application generates the next target location for the drone.
The motion planner computes a sequence of waypoints from the current location to the target location -- a motion plan.
The waypoints $w_1\dots w_6$ in Figure~\ref{fig:casestudy} represent one such motion plan generated by the planner and the dotted lines represent the reference trajectory for the drone.
Once the motion primitive library receives the next waypoint, it generates the required low-level controls necessary to closely follow the reference trajectory.
The solid trajectory in Figure~\ref{fig:casestudy} represents the actual trajectory of the drone, which deviates from the reference trajectory because of the underlying dynamics.
Programming such robotics software stack is challenging as it is composed of individual components, each implementing a complicated protocol, and
continuously interacting with each other for accomplishing the mission safely.

In our drone surveillance case study, we would like the system to satisfy two safety invariants:
\point{1} {\textit{Obstacle Avoidance} ($\phi_{obs}$): The drone must never collide with any obstacle.
\point{2} {\textit{Battery Safety}} ($\phi_{bat}$): The drone must never crash because of low battery. Instead, when the battery is low it must prioritize landing safely (e.g., in Figure~\ref{fig:casestudy} (right), low battery is detected at $w_6$ and the mission is aborted to land safely).
$\phi_{obs}$ can be further decomposed into two parts $\phi_{obs}:= \phi_{plan} \wedge \phi_{mpr}$;
\point{a} {\textit{Safe Motion Planner}} ($\phi_{plan}$): The motion planner must always generate a motion-plan such that the reference trajectory does not collide with any obstacle,
\point{b} {\textit{Safe Motion Primitives}} ($\phi_{mpr}$): When tracking the reference trajectory between any two waypoints generated by the motion planner, the controls generated by the motion primitives must ensure that the drone closely follows the trajectory and avoids collisions.

In practice, when implementing the software stack, the programmer may use several uncertified components (red blocks in Figure~\ref{fig:softwarestack}).
For example, implementing an on-the-fly motion planner may involve solving an optimization problem or using an efficient search technique that relies on a solver or a third-party library (e.g., OMPL~\cite{ompl}).
Similarly, motion primitives are either designed using machine-learning techniques like Reinforcement Learning~\cite{kaelbling1996reinforcement}, or optimized for specific tasks without considering safety, or are off-the-shelf controllers provided by third parties~\cite{px4}.
Ultimately, in the presence of such uncertified or hard to verify components, it is difficult to provide formal guarantees of safety at design time.
We assume the state-estimators (green blocks) in Figure~\ref{fig:softwarestack} are trusted and accurately provide the system state within bounds.

\noindent
\textbf{Challenges and motivation:}
The robotics software (Figure~\ref{fig:softwarestack}) must react to events (inputs) from the physical
world as well as other components in the software stack. These components must therefore be implemented as concurrent event-driven software which can be notoriously tricky to test and debug due to nondeterministic interactions with the environment and interleaving of the event handlers.
In \text{\small \textsc{Soter}}\xspace, we provide a language framework for both implementing and systematic testing of such event-driven software.
In practice, for complex systems, it can be extremely difficult to design a controller that is both safe and high-performance.
The AC, in general, is any program or component designed for high-performance under nominal conditions using either third-party libraries or machine-learning techniques.
We treat them as unsafe since they often exhibit unsafe behavior in off-nominal conditions and uncertain environments, and even when they do not, it is hard to be sure since their complexity makes verification or exhaustive testing prohibitively expensive.
Furthermore, the trend in robotics is towards {\em{advanced}}, data-driven controllers, such as those based on neural networks (NN), that usually do not come with safety guarantees.
Our approach of integrating \textsc{RTA}\xspace into a programming framework is motivated by the need to enable the use of such advanced controllers (e.g., designed using NN or optimized for performance) while retaining strong guarantees of safety.

\subsection{Programming Reactive Robotic Software}
The Robot Operating System (ROS~\cite{ROS}) is an open-source meta-operating system considered as the de facto standard
for robot software development.
In most cases, a ROS programmer implements the system as a collection of periodic processes that communicates using the publish-subscribe model of communication.
\text{\small \textsc{Soter}}\xspace provides a high-level domain specific language based on a similar publish-subscribe model of communication.
A program in \text{\small \textsc{Soter}}\xspace is a collection of periodic \textit{nodes} (processes) communicating with each other by publishing on and subscribing to message topics.
A node periodically listens to data published on certain topics, performs computation, and publishes
computed results on certain other topics.  A topic is an abstraction of a communication channel.

\noindent
\textbf{Topics.}
Figure~\ref{fig:nodes} declares the topic \codename{targetWaypoint} that can be used to communicate messages of type \codename{coord} (coordinates in 3D space). In \text{\small \textsc{Soter}}\xspace, a node communicates with other nodes in the system by publishing messages on a topic (e.g., \codename{targetWaypoint}) and the target nodes can consume these messages by subscribing to it.

\begin{figure}[h]
	\centering
	\vspace{-0.4cm}
	\includegraphics[scale=0.35]{code/nodes.png}
	\vspace{-0.7cm}
	\caption{Declaration of topics and nodes in \text{\small \textsc{Soter}}\xspace}
	\vspace{-0.2cm}
	\label{fig:nodes}
\end{figure}

\noindent
\textbf{Nodes.}
Figure~\ref{fig:nodes} also declares a node \codename{MotionPrimitive} that subscribes to topics \codename{localPosition} and \codename{targetWaypoint}.
Each node has a separate local buffer associated with each subscribed topic.
The publish operation on a topic adds the message into the corresponding local buffer of all the nodes that have subscribed to that topic.
The \codename{MotionPrimitive} node runs periodically every 10 $ms$.
It reads messages from the subscribed topics, performs local computations, and then publishes the control action on the output topic.
For the exposition of this paper, we ignore the syntactic details of the node body, it can be any sequential program that performs the required read $\rightarrow$ compute $\rightarrow$ publish step.

\subsection{Guaranteeing Safety using Runtime Assurance}
In practice, the motion primitives (e.g., \codename{MotionPrimitive} node in Figure~\ref{fig:nodes}) might generate control actions to traverse the reference trajectory from current position to the target waypoint using a low-level controller provided by the third-party robot manufacturer (e.g.,~\cite{px4}). These low-level controllers generally use approximate models of the dynamics of the robot and are optimized for performance rather than safety, making them unsafe.

\begin{figure}[h]
	\centering
	\includegraphics[scale=0.3]{figures/combexp.png}
	\vspace{-0.25cm}
	\caption{Experiments with third-party and machine-learning controllers}
	\label{fig:controllerexp}
\end{figure}

To demonstrate this, we experimented with the low-level controllers provided by the PX4 Autopilot~\cite{px4} (Figure~\ref{fig:controllerexp} (right)).
The drone was tasked to repeatedly visit locations $g_1$ to $g_4$ in that order, i.e., the sequence of waypoints {\small $g_1, \dots g_4$} are passed to the \codename{MotionPrimitive} node.
The blue lines represent the actual trajectories of the drone.
Given the complex dynamics of a drone and noisy sensors, ensuring that it precisely follows a fixed trajectory (ideally a straight line joining the waypoints) is extremely hard.
The low-level controller (untrusted) optimizes for time and, hence, during high speed maneuvers the reduced control on the drone leads to overshoot and trajectories that collide with obstacles (represented by the red regions).
We also conducted similar experiment with a different low-level controller designed using data-driven approach (Figure~\ref{fig:controllerexp} (left)) where we tasked the drone to follow a eight loop. The trajectories in green represent the cases where the drone closely follows loop, the trajectories in red represent the cases the drone dangerously deviates from the reference trajectory.
Note that in both cases, the controllers can be used during majority of their mission except for a few instances of unsafe maneuvers.
This motivates the need for a \textsc{RTA}\xspace system that guarantees safety by switching to a safe controller in case of danger but also maximizes the use of the untrusted but performant controller under nominal conditions.

\noindent
\textbf{Runtime Assurance module.}
Figure~\ref{fig:simplextube} illustrates the behavior of a \text{\small \textsc{Soter}}\xspace based \textsc{RTA}\xspace-protected motion primitive module.

\begin{figure}[h]
	\vspace{-0.2cm}
	\centering
	\includegraphics[scale=0.3]{figures/simplextube}
	\vspace{-0.2cm}
	\caption{An \textsc{RTA}\xspace-protected Motion Primitive}
	\label{fig:simplextube}
\end{figure}

We want the drone to move from its current location $w_i$ to the target location $w_f$, and the desired safety property is that the drone must always remain inside the region $\phi_{safe}$ (outermost tube).
Initially, the untrusted {\sc AC}\xspace node (e.g., \codename{MotionPrimitive}) is in control of the drone (red trajectory), and since it is not certified for correctness it may generate controls action that tries to push the drone outside the $\phi_{safe}$ region.
If {\sc AC}\xspace is wrapped inside an \textsc{RTA}\xspace module (see Figure~\ref{fig:simplexarchitecture}) then {\sc DM}\xspace must detect this imminent danger and switch to {\sc SC}\xspace (blue trajectory) with enough time for {\sc SC}\xspace to gain control over the drone.
{\sc SC}\xspace must be certified to keep the drone inside $\phi_{safe}$ and also move it to a state in $\phi_{safer}$ where {\sc DM}\xspace evaluates that it is safe enough to return control back to {\sc AC}\xspace.
The novel aspect of an \textsc{RTA}\xspace module formalized in this paper is that {\em it also allows control to return back to {\sc AC}\xspace to maximize performance}.

\begin{figure}[h]
	\centering
	\vspace{-0.4cm}
	\includegraphics[scale=0.45]{code/rtamodule.png}
	\vspace{-0.4cm}
	\caption{Declaration of an \textsc{RTA}\xspace module}
	\vspace{-0.2cm}
	\label{fig:rtamodule}
\end{figure}

Figure~\ref{fig:rtamodule} presents the declaration of an \textsc{RTA}\xspace module consisting of \codename{MotionPrimitive} (from Figure~\ref{fig:nodes}) and \codename{MotionPrimitiveSC} as {\sc AC}\xspace and {\sc SC}\xspace nodes.
The compiler checks that the declared \textsc{RTA}\xspace module \codename{SafeMotionPrimitive} is well-formed (Section~\ref{sec:correctness}) and then generates the {\sc DM}\xspace and the other glue code that together guarantees the $\phi_{safe}$ property.
Details about other components of the module declaration are provided in Section~\ref{sec:correctness}.

\noindent
\textbf{Compositional \textsc{RTA}\xspace System.} A large system is generally built by composing multiple components together.
When the system-level specification is decomposed into a collection of simpler component-level specifications, one can scale provable guarantees to large, real-world systems.

\begin{figure}[h]

	\centering
	\vspace{-0.3cm}
	\includegraphics[scale=0.35]{figures/protectedsoft.png}
	\caption{{An \textsc{RTA}\xspace Protected Software Stack for Drone Surveillance}}
	\vspace{-0.2cm}
	\label{fig:rtasoftwarestack}
\end{figure}

\text{\small \textsc{Soter}}\xspace enables building a \textit{reliable} version (Figure~\ref{fig:rtasoftwarestack}) of the software stack with \textit{runtime assurance} of the safety invariant: $\phi_{plan} \wedge \phi_{mpr} \wedge \phi_{bat}$.
We decompose the stack into three components: \point{1} An \textsc{RTA}\xspace-protected motion planner that guarantees $\phi_{plan}$, \point{2} A battery-safety \textsc{RTA}\xspace module that guarantees $\phi_{bat}$, and \point{3} An \textsc{RTA}\xspace-protected motion primitive module that guarantees $\phi_{mpr}$.
Our theory of well-formed \textsc{RTA}\xspace modules (Theorem~\ref{thm:rta}) ensures that if the constructed modules are well-formed then they satisfy the desired safety invariant and their composition (Theorem~\ref{thm:comp}) helps prove that the system-level specification is satisfied.

\section{Related Work}

\label{sec:relatedwork}
We next situate \text{\small \textsc{Soter}}\xspace with related techniques for building robotics systems with high-assurance of correctness~\cite{GUIOCHET201743}.

\noindent
\textbf{Reactive synthesis.}
There is increasing interest towards synthesizing reactive robotics controllers from temporal logic~\cite{kress2009temporal,fainekos2009temporal,saha2014automated,shoukry-cdc17}.
Tools like TuLip~\cite{tulip}, BIP~\cite{bensalem2013verifiable,bip2012}, and LTLMoP~\cite{ltlmop} construct a finite transition system that serves as
an abstract model of the physical system and synthesizes a strategy, represented by a finite state automaton, satisfying
the given high-level temporal specification.
Though the generated strategy is guaranteed to be safe in the
abstract model of the environment, this approach has limitations: (1) there is gap between the abstract models of the system and its actual behavior in the physical world; (2) there is gap between the generated strategy state-machine and its actual software implementation that interacts with the low-level controllers; and finally (3) the synthesis approach scale poorly both with the complexity of the mission and the size of the workspace.
Recent tools such as SMC~\cite{shoukry-cdc17} generate both high-level and low-level
plans, but still need additional work to translate these plans into reliable software on top of robotics platforms.

\noindent
\textbf{Reachability analysis and Simulation-based falsification.}
Reachability analysis tools~\cite{FrehseLGDCRLRGDM11,chen2013flow,duggirala2015c2e2} have been used to verify robotics systems modeled as hybrid systems.
Differently from our work, reachability methods require an explicit representation of the robot dynamics and often suffer from scalability issues when the system has a large number of discrete states.
Also, the analysis is performed using the models of the system, and hence, there is a gap between the models being verified and their implementation.
Simulation-based tools for the falsification of CPS models (e.g.,~\cite{DreossiDS17}) are more scalable than reachability methods, but generally, they do not provide any formal guarantees.
In this approach, the entire robotics software stack is tested by simulating it in a loop with a high-fidelity model of the robot and hence, this approach does not suffer from the gap between model and implementation described in the previous approaches.
However, a challenge to achieving scalable coverage comes from the considerable time it can take for simulations.

\noindent
\textbf{Runtime Verification and Assurance.}
Runtime verification has been applied to robotics~\cite{pettersson2005execution,DesaiRV2017,deshmukh2017robust,huang2014rosrv,permis,LiW08,HofmannW06} where online monitors are used to check the correctness (safety) of the robot at runtime.
Schierman \textit{et al.}~\cite{schierman2015runtime} investigated how the $\textsc{RTA}\xspace$ framework can be used at different levels of the software stack of an unmanned aircraft system. In a more recent work~\cite{phan2017component}, Schierman \textit{et. al.} proposed a component-based simplex architecture (CBSA) that combines assume-guarantee contracts with \textsc{RTA}\xspace for assuring the runtime safety of component-based cyber-physical systems.
In~\cite{sandboxingcontrollers}, the authors apply simplex approach for sandboxing cyber-physical systems and present automatic reachability based approaches for inferring switching conditions.
The idea of using an advanced controller ({\sc AC}\xspace) under nominal conditions; while at the boundaries, using optimal safe control ({\sc SC}\xspace) to maintain safety has also been used in~\cite{reachabilitysafelearning} for operating quadrotors in the real world.
In~\cite{Aswaniquad} the authors use a switching architecture (\cite{LBMPC}) to switch between a nominal safety model and learned performance model to synthesize policies for a quadrotor to follow a trajectory.
Recently, ModelPlex~\cite{Mitsch2016} combines offline verification of CPS models with runtime validation of system executions for compliance with the model to build correct by construction runtime monitors which provides correctness guarantees for CPS executions at runtime.
Note that most prior applications of \textsc{RTA}\xspace do not provide high-level programming language support for constructing provably-safe \textsc{RTA}\xspace systems
in a compositional fashion while designing for {\em timing and communication behavior} of such systems.
They are all instances of using \textsc{RTA}\xspace as a \textit{design methodology} for building reliable systems in the presence of untrusted components.

\noindent
\textbf{\text{\small \textsc{Soter}}\xspace approach.}
In order to ease the construction of \textsc{RTA}\xspace systems, there is a need
for a general programming framework that supports run-time assurance principles and also considers implementation aspects such as timing and communication.
Our approach is to provide a high-level language to
(1) enable programmers to implement and specify the complex reactive system,
(2) leverage advances in scalable systematic-testing techniques for validation of the actual implementation of the software, and
(3) provide language support for runtime assurance to ensure safety in the real physical world.
We formalize a generic runtime assurance architecture and implement it in programming framework for mobile robotic systems.
We demonstrate the efficacy of \text{\small \textsc{Soter}}\xspace framework by building a real-world drone software stack and conducted rigorous experiments to demonstrate safety of autonomous robots in the presence of untrusted components.
Also, note that most of the work done in the context of runtime assurance techniques provide solutions where the switching logic in {\sc DM}\xspace is only configured to switch the control from {\sc AC}\xspace to {\sc SC}\xspace. In our architecture, the programmer can also specify the condition under which to transfer control back to {\sc AC}\xspace, and maximize the use of {\sc AC}\xspace during a mission.

\subsection{Correctness of an \textsc{RTA}\xspace\ Module}
\label{sec:correctness}

Given a safe set $\phi_{safe}$, our goal is to prove that the \textsc{RTA}\xspace-protected system always stays inside this safe set.
We need the \textsc{RTA}\xspace\ module to satisfy some additional conditions in order to prove its safety.

\noindent
\textbf{Well-formed \textsc{RTA}\xspace Module.}
An \textsc{RTA}\xspace module $M = (\ensuremath{N_{ac}}, \ensuremath{N_{sc}}, \ensuremath{N_{dm}}, \ensuremath{\Delta}, \phi_{safe}, \phi_{safer})$ is said to be {\em{well-formed}}
if its components satisfy the following properties:

\noindent
\cond{P1a} The maximum period of $\ensuremath{N_{ac}}$ and $\ensuremath{N_{sc}}$ is $\ensuremath{\Delta}$, i.e., $\Period{\ensuremath{N_{dm}}} = \Delta$, $\Period{\ensuremath{N_{ac}}} \leq \Delta$, and $\Period{\ensuremath{N_{sc}}} \leq \Delta$.

\noindent
\cond{P1b} The output topics of the $\ensuremath{N_{ac}}$ and $\ensuremath{N_{sc}}$ nodes must be same, i.e., $\Outputs{\ensuremath{N_{ac}}} = \Outputs{\ensuremath{N_{sc}}}$.

\noindent
The safe controller, $\ensuremath{N_{sc}}$, must satisfy the following properties:

\noindent
\cond{P2a} (\textit{Safety}) $\ensuremath{Reach}_{M}(\phi_{safe},\ensuremath{N_{sc}},\infty)\subseteq \phi_{safe}$. This property ensures that if the system is in $\phi_{safe}$, then it will remain in that region as long as we use $\ensuremath{N_{sc}}$.

\noindent
\cond{P2b} (\textit{Liveness})
For every state ${s}\in\phi_{safe}$, there exists a time $T$ such that for all $s' \in \ensuremath{Reach}_{M}({s}, \ensuremath{N_{sc}}, T)$, we have
$\ensuremath{Reach}_{M}({s}',\ensuremath{N_{sc}},\ensuremath{\Delta}) \subseteq \phi_{safer}$.
In words, from every state in $\phi_{safe}$, after some finite time the system is guaranteed to stay in $\phi_{safer}$ for at least $\Delta$ time.

\noindent
\cond{P3}
	$\ensuremath{Reach}_{M}(\phi_{safer}, *, 2\Delta) \subseteq \phi_{safe}$. This condition says that irrespective of the controller, if we start from a state in $\phi_{safer}$, we will continue to remain in $\phi_{safe}$ for $2\ensuremath{\Delta}$ time units. Note that this condition is stronger than the condition $\phi_{safer} \subseteq \phi_{safe}$.

\vspace{0.2cm}
\begin{thm}[{\sc \textbf{Runtime Assurance}}]
	\textit{For a well-formed \textsc{RTA}\xspace module $M$, let ${\phi_{\mathtt{Inv}}}(\texttt{mode},{s})$ denote the predicate $(\texttt{mode=SC} \wedge {s}\in\phi_{safe}) \vee (\texttt{mode=AC} \wedge \ensuremath{Reach}_{M}({s}, *,\ensuremath{\Delta})\subseteq\phi_{safe})$.
	If the initial state satisfies the invariant ${\phi_{\mathtt{Inv}}}$,
	then every state ${s}_t$ reachable from ${s}$ will also satisfy the invariant
	${\phi_{\mathtt{Inv}}}$.}

	\label{thm:rta}
\end{thm}
\vspace{0.2cm}
\textit{Proof.}
	Let $(\texttt{mode},{s})$ be the initial mode and initial state of the system.
	We are given that the invariant holds at this state.
	Since the initial mode is {\sc SC}\xspace,  then, by assumption, ${s}\in\phi_{safe}$.
	We need to prove that all states ${s}_t$ reachable from ${s}$ also satisfy the invariant.
	If there is no mode change, then invariant is satisfied by Property~\cond{P2a}.
	Hence, assume there are mode switches.
	We prove that in every time interval between two consecutive executions of the {\sc DM}\xspace, the invariant holds.
	So, consider time $T$ when the {\sc DM}\xspace executes.
	\\
	(Case1)
	The mode at time $T$ is {\sc SC}\xspace and there is no mode switch at this time.
	Property \cond{P2a} implies that all future states will satisfy the invariant.
	\\
	(Case2)
	The mode at time $T$ is {\sc SC}\xspace and there is a mode switch to the {\sc AC}\xspace at this time.

	Then, the current state ${s}_T$ at time $T$ satisfies the condition ${s}_T\in\phi_{safer}$.
	By Property~\cond{P3}, we know that $\ensuremath{Reach}_{M}({s}_T,*,2\Delta) \subseteq \phi_{safe}$, and hence,
	it follows that
	$\ensuremath{Reach}_{M}({s}_T,*,\Delta) \subseteq \phi_{safe}$, and hence the invariant ${\phi_{\mathtt{Inv}}}$ holds at time $T$.
	In fact, irrespective of what actions {\sc AC}\xspace\ applies to the plant, Property~\cond{P3} guarantees that
	the invariant will hold for the interval $[T,T+\ensuremath{\Delta}]$.
	Now, it follows from Property~\cond{P1} that the {\sc DM}\xspace\ will execute again at or before
	the time instant $T+\ensuremath{\Delta}$, and hence the invariant holds until the next execution of {\sc DM}\xspace.
	\\
	(Case3)
	The current mode at time $T$ is {\sc AC}\xspace and there is a mode switch to {\sc SC}\xspace at this time.
	Then, the current state ${s}_T$ at time $T$ satisfies the condition
	$\ensuremath{Reach}_{M}({s}_T,*,2\ensuremath{\Delta})\not\subseteq\phi_{safe}$.
	Since the mode at time $T-\epsilon$ was still {\sc AC}\xspace, and by inductive hypothesis we know that the
	invariant held at that time; therefore,
	we know that $\ensuremath{Reach}_{M}({s}_{T-\epsilon}, *,\ensuremath{\Delta})\subseteq\phi_{safe}$. Therefore,
	for the period $[T-\epsilon,T-\epsilon+\ensuremath{\Delta}]$, we know that the reached state will be in
	$\phi_{safe}$ and the invariant holds.
	Moreover, {\sc SC}\xspace will get a chance to execute in this interval at least once, and
	hence, from that time point onwards, Property~\cond{P2a} will guarantee that the invariant holds.
	\\
	(Case4)
	The current mode at time $T$ is {\sc AC}\xspace and there is a no mode switch.
	Since there is no mode switch at $T$, it implies that
	$\ensuremath{Reach}_{M}({s}_T,*,2\ensuremath{\Delta}) \subseteq \phi_{safe}$ and hence for the next $\ensuremath{\Delta}$ time units,
	we are guaranteed that
	$\ensuremath{Reach}_{M}({s}_T,*,\ensuremath{\Delta}) \subseteq \phi_{safe}$ holds.

\vspace{0.2cm}

The invariant established in Theorem~\ref{thm:rta} ensures that if the assumptions of the
theorem are satisfied, then all reachable states are always contained in $\phi_{safe}$.

\vspace{0.2cm}
\begin{remark}[{\bf Guarantee switching and avoid oscillation}]
	The liveness property~\cond{P2b} guarantees that the system will definitely switch from $\ensuremath{N_{sc}}$ to $\ensuremath{N_{ac}}$ (to maximize performance).
	Property~\cond{P3} ensures that the system will stay in the {\sc AC}\xspace mode for some time and not switch back immediately to the {\sc SC}\xspace mode.
	Note that property~\cond{P2b} is not needed for Theorem~\ref{thm:rta}.
\end{remark}
\vspace{0.2cm}

\begin{remark}[{\bf {\sc AC}\xspace is a black-box}]
Our well-formedness check does not involve proving anything about
$\ensuremath{N_{ac}}$.
\cond{P1a} and \cond{P1b} require that $\ensuremath{N_{ac}}$ samples at most as fast as $\ensuremath{N_{dm}}$ and generates the same outputs as $\ensuremath{N_{sc}}$, this is for smooth transitioning between $\ensuremath{N_{ac}}$ and $\ensuremath{N_{sc}}$.
We only need to reason about $\ensuremath{N_{sc}}$, and we need to reason about all possible
controller actions (when reasoning with $\ensuremath{Reach}_{M}({s},*,\ensuremath{\Delta})$). The latter
is worst-case analysis, and includes $\ensuremath{N_{ac}}$'s behavior.  One could restrict
behaviors to $\ensuremath{N_{ac}}\cup \ensuremath{N_{sc}}$ if we wanted to be more precise, but then $\ensuremath{N_{ac}}$ would
not be a black-box anymore.
\end{remark}
\vspace{0.2cm}

Our formalism makes no assumptions about the code (behavior) of the AC node, except that we do need to know the set of all possible output actions (required for doing worst-case reachability analysis). Theorem 3.1 ensures safety as long as all output actions generated by the code {\sc AC}\xspace (like in Figure~\ref{fig:nodes}) belong to the assumed set of all possible actions.

\begin{defn}[{\bf Regions}]
Let $\SR{\phi}{t} = \{ s \mid s\in \phi \wedge \ensuremath{Reach}_{M}(s, *, t) \subseteq \phi \}$. For example, $\SR{\phi_{safe}}{\Delta}$ represents the region or set of states in $\phi_{safe}$ from which all reachable states in time $\Delta$ are still in $\phi_{safe}$.
\end{defn}

\noindent
\textbf{Regions of operation of a well-formed \textsc{RTA}\xspace module.}
We informally describe the behavior of an \textsc{RTA}\xspace protected module by organizing the state space of the system into different regions of operation (Figure~\ref{fig:regions}).
R1 represents the unsafe region of operation for the system.
Regions R2-R5 represent the safe region and R3-R5 are the recoverable regions of the state space.
The region R3$\setminus$R4 represents the \textit{switching control} region (from {\sc AC}\xspace to {\sc SC}\xspace) as the time to escape $\phi_{safe}$ for the states in this region is less than $2\ensuremath{\Delta}$.

\begin{wrapfigure}{l}{0.6\columnwidth}
	\centering
	\includegraphics[scale=0.33]{figures/regions.png}
	\vspace{-0.75cm}
	\caption{Regions of Operation for an \textsc{RTA}\xspace Module.}
	\vspace{-0.3cm}
	\label{fig:regions}
\end{wrapfigure}

As the {\sc DM}\xspace is guaranteed to sample the state of the system at least once in $\ensuremath{\Delta}$ time (property \cond{P1a}), the {\sc DM}\xspace is guaranteed to switch control from {\sc AC}\xspace to {\sc SC}\xspace if the system remains in the switching control region for at least $\ensuremath{\Delta}$ time, which is the case before system can leave region R3.
Consider the case where T1 represents a trajectory of the system under the influence of {\sc AC}\xspace, when the system is in the switching control region the {\sc DM}\xspace detects the imminent danger and switches control to {\sc SC}\xspace. \cond{P1a} ensures that $\ensuremath{N_{sc}}$ takes control before the system escapes $\phi_{safe}$ in the next $\Delta$ time. Property \cond{P2a} ensures that the resultant trajectory T2 of the system remains inside the safe region and Property \cond{P2b} ensures that the system eventually enters region R5 where the control can be returned to {\sc AC}\xspace for maximizing the performance of the system. Property \cond{P3} ensures that the switch to {\sc AC}\xspace is safe and the system will remain in {\sc AC}\xspace mode for at least $\ensuremath{\Delta}$ time.

\vspace{0.2cm}
\begin{remark}[{\bf Choosing $\phi_{safer}$ and $\Delta$}]
	The value of $\Delta$ is critical for ensuring safe switching from {\sc AC}\xspace to {\sc SC}\xspace.
	It also determines how conservatively the system behaves: for example, large value of $\Delta$ implies a large distance between boundaries of region R4 and R5 during which {\sc SC}\xspace (conservative) is in control.
	Small values of $\Delta$ and a larger R5 region ($\phi_{safer}$) can help maximize the use of {\sc AC}\xspace but might increase the chances of switching between {\sc AC}\xspace and {\sc SC}\xspace as the region between the boundaries of R4 and R5 is too small.
	Currently, we let the programmer choose these values and leave the problem of automatically finding the optimal values as future work.
\end{remark}
\vspace{0.2cm}

\noindent
\textbf{From theory to practice:}
We are assuming here that the checks in Property~\cond{P2} and Property~\cond{P3} can be
performed. The exact process for doing so is outside the scope of this paper.
The popular approach in control theory is to use reachability analysis when designing an $\ensuremath{N_{sc}}$ that always keeps the system within a set of safe states. We used existing tools like FastTrack~\cite{herbert2017fastrack} and the Level-Set Toolbox~\cite{FrehseLGDCRLRGDM11}.

First, consider the problem of synthesizing the safe controller $\ensuremath{N_{sc}}$ for a given
safe set $\phi_{safe}$.
$\ensuremath{N_{sc}}$ can be synthesized using pre-existing safe control synthesis techniques.
For example, for the motion primitives, we can use a framework like FaSTrack~\cite{herbert2017fastrack} for synthesis of low-level $\ensuremath{N_{sc}}$.
Next, we note that the {\sc DM}\xspace needs to reason about the reachable set of states for a system when
either the controller is fixed to $\ensuremath{N_{sc}}$ or is nondeterministic.
Again, there are several tools and techniques for performing reachability computations~\cite{FrehseLGDCRLRGDM11}.
One particular concept that \text{\small \textsc{Soter}}\xspace requires here is the notion of {\em{time to failure less than 2$\Delta$}} ($\mathtt{ttf}_{2\Delta}$).
The function $\mathtt{ttf}_{2\Delta} : \mathcal{S} \times 2^{\mathcal{S}} \rightarrow \mathbb{B}$, given a state $s \in \mathcal{S}$ and a predicate $\phi \subseteq \mathcal{S}$ returns {\em true} if starting from $s$, the minimum time after which $\phi$ may not hold is less than or equal to $2\Delta$.
The check $\ensuremath{Reach}(s_t,*,2\ensuremath{\Delta}) \not\subseteq\phi_{safe}$ in Figure~\ref{fig:dmlogic} can be equivalently described using the $\mathtt{ttf}_{2\Delta}$ function as $\mathtt{ttf}_{2\Delta}(s_t, \phi_{safe})$.
Let us revisit the boolean functions \codename{PhiSafer\_MPr} and \codename{TTF2D\_MPr} from Figure~\ref{fig:rtamodule}, these functions correspond to the checks $s_t \in \phi_{safer}$ and $\mathtt{ttf}_{2\Delta}(s_t, \phi_{safe})$ respectively.

\input{semantics}

\subsection{Obstacle Collision Avoidance}

\label{Sec:safe_MPR}
Given a high level task to visit a goal location, the motion planner computes a motion plan (sequence of motion primitives); such that the low level motion primitives can safely take the robot to the goal while avoiding collisions.
In our case, motion plan is a sequence of $\mathtt{goto}$ primitives.
The motion planner  assumes that the trajectory of a robot when executing the $\mathtt{goto}$ primitive always lies inside a bounded tube.
In other words, if $\xi$ represents the trajectory of the robot when executing primitive $\mathtt{goto}(\mathbf{x}_f)$ at location $\mathbf{x}_i$ and if $\xi(t)$ represents the position of the robot in the trajectory at time $t$ then we require, $\forall t, \xi(t) \in \tube{(\mathbf{x}_i,\mathbf{x}_f)}{\epsilon}$ for some $\epsilon$.
We refer to $\tube{(\mathbf{x}_i,\mathbf{x}_f)}{\epsilon}$ as the \textit{safe-tube} for a motion-primitive $\mathtt{goto}(\mathbf{x}_f)$ applied at position $\mathbf{x}_i$.
To guarantee collision avoidance, the motion planner must then ensure that the $\epsilon$-tube surrounding the sequence of $\mathtt{goto}$ primitives does not collide with any obstacle.

The hard problem is computing the value of $\epsilon$ for the tube such that the $goto$ primitive provides the guarantee that any trajectory executed by it keeps the robot within the $\epsilon$-tube.
Since these motion primitives are implemented using off-the-shelf controllers or learned controllers providing such guarantees is extremely hard.

\begin{wrapfigure}{l}{0.6\columnwidth}
	\centering
	\includegraphics[scale=0.3]{figures/tube}
	\caption{Experiment to demonstrate that $\mathtt{goto}$ implemented using untrusted third-party controllers is unsafe}
	\label{fig:tubeexp}
\end{wrapfigure}

\noindent
\textbf{Experiment:} To demonstrate this problem, we experimented with a $\mathtt{goto}$ primitive implemented using controllers provided by the drone manufacturers. Figure~\ref{fig:tubeexp} presents the workspace consisting of a square track surround by obstacles on all sides (dashed gray area). The task for the drone was to repeatedly visit locations g1 to g4 in that order which corresponds to a motion plan {\small $\mu = \mathtt{goto}(g1)\mathtt{goto}(g2)..\mathtt{goto}(g4)$}.
The blue lines represent the trajectories of the drone.
The green region represents the safe-tube for the $\mathtt{goto}$ primitives.  The $\epsilon$ is chosen such that the tube does not collide with the obstacles.
Given the complex dynamics of a drone and noisy sensors, ensuring that the drone precisely follows a fixed trajectory (ideally a straight line joining the goal locations) is extremely hard.
The untrusted low-level controllers used for implementing the $\mathtt{goto}$ optimizes for speed and tries to minimize the time taken to cover each segment.
Optimizing for high speed maneuvers reduces the control on the drone which leads to overshoot and trajectories that can lead to collisions (represented by the red regions).

\begin{wrapfigure}{l}{0.6\columnwidth}
    	\centering
	\includegraphics[scale=0.23]{figures/simplextube}
	\caption{Regions of operation for \textsc{RTA}\xspace protected $\mathtt{goto}$ motion primitive}
	\label{Fig:goto}
\end{wrapfigure}

\noindent
\textbf{$\textsc{RTA}\xspace$ protected safe $\mathtt{goto}$:}
We next show how we construct a safe $\mathtt{goto}$ primitive by wrapping it inside a \textsc{RTA}\xspace module.
Figure~\ref{Fig:goto} presents the behavior of a safe $\mathtt{goto}$ represented by the \textsc{RTA}\xspace module $M_{rta}= (f_{AC}, f_{SC}, \ensuremath{\Delta}, \phi_{safe}, \phi_{safer})$ where:
(1) {$f_{AC}$} is a $\mathtt{goto}$ motion primitive implemented using untrusted controllers optimizing the time taken to reach $\mathbf{x}_{f}$ as fast as possible.
(2) {$f_{SC}$} is a safe controller that maintains the trajectory within the $tube(\mathbf{x}_{i}, \mathbf{x}_{f}, \epsilon)$. One can implement $f_{SC}$ to be a low level controller designed for safety and that moves the drone from its current location $\mathbf{x}_t$ in the switching region to a location inside $S(\phi_{safer}, \ensuremath{\Delta})$ (represented by the blue trajectory). Potential candidates for $f_{SC}$ are bang-bang controller~\cite{bellman1956bang} or iterative linear quadratic regulators (iLQR)~\cite{DBLP:conf/icinco/LiT04}. $f_{SC}$ must satisfy the well-formedness constraints {\footnotesize \cond{P2}} of the \textsc{RTA}\xspace module.
(3) $\ensuremath{\Delta}$ is chosen when designing $f_{SC}$ as it must satisfy {\footnotesize \cond{P2}}.
(4) $\phi_{safe}$ asserts that the current position $ \mathbf{x}_t \in tube(\mathbf{x}_{i}, \mathbf{x}_{f}, \epsilon)$. The region inside the outermost tube is the safe region for the \textsc{RTA}\xspace module.
(5) $\phi_{safer}$ is chosen such that $\phi_{safer}$, $\phi_{safe}$ and $\ensuremath{\Delta}$ jointly satisfy {\footnotesize \cond{P3}} and is represented by the innermost tube.

To compute $\mathtt{ttf}(\mathbf{x}, \phi_{safe})$ accurately, we need to know the dynamics of the system. We can compute $\mathtt{ttf}(\mathbf{x}, \phi_{safe})$, by exhaustively searching over all trajectories starting from $\mathbf{x}$, and picking the smallest trajectory which leaves $\SR{\phi_{safe}}{0}$. This computation is time consuming with poor scaling with dimension of $\mathbf{x}$.
In practice, we can get a conservative upper bound for $\mathtt{ttf}(\mathbf{x}, \phi_{safe})$, by making the assumption that the underlying dynamics is continuous and Lipschitz bounded.
This is a reasonable assumption to make since all physical systems are continuous, and are locally Lipschitz bounded given the control space, $\mathcal{U}$, is bounded.
A good approximation of the local Lipschitz bound with respect to the control is, $L_{u} = \max \frac{\partial f}{\partial u}(\mathbf{x}, u)$.  Given $L_u$, we can compute the conservative $\hat{\mathtt{ttf}}(\mathbf{x}, \phi_{safe}) = d_{min}(\partial\SR{\phi_{safe}}{0}, \mathbf{x})/L_{u}$, where $\partial\SR{\phi_{safe}}{0}$ is the boundary of the safe set, and $d_{min}(\partial\SR{\phi_{safe}}{0}, \mathbf{x})$ is minimum distance between $\mathbf{x}$ and the boundary, $\partial\SR{\phi_{safe}}{0}$ . In our drone experiment, $L_{u}$ depends on the maximum torque input, and $\partial\SR{\phi_{safe}}{0}$ is the circumference of the safe-tube.

In Figure~\ref{Fig:goto}, the {\sc DM}\xspace monitors the trajectory generated by $f_{AC}$ to check if the trajectory leaves $\phi_{safe}$ and transfers control to $f_{SC}$ once it leaves the $S(\phi_{safe}, 2*\ensuremath{\Delta})$ tube.
The $f_{SC}$ is responsible for returning the drone to $S(\phi_{safer}, \ensuremath{\Delta})$, where the {\sc DM}\xspace returns control back to $f_{AC}$ in order to maximize the usage of {\sc AC}\xspace.
More details about the safe $\mathtt{goto}$ and its evaluation is provided in Section~\ref{sec:tuberesults}.

Note that $M_{rta}$ guarantees that all trajectories of the drone will remain inside the corresponding safe-tube irrespective of the implementation of the $\mathtt{goto}$ primitive i.e. $f_{AC}$.
\textit{This is the advantage of using \textsc{RTA}\xspace as one can now substitute $f_{AC}$ with any controller which maybe faulty, but the system would still remain within the safe-tube.}
The motion planner that uses the safe $\mathtt{goto}$ motion primitives now provide the guarantee of no obstacle collision as long as it ensures that the safe-tubes do not collide with the obstacles.

\subsection{Runtime Assurance for Safe Exploration}

When operating in environments which are unknown \textit{a-priori}, a robot faces the challenge of exploring the environment safely and still accomplishing the desired goal.
A large body of research, classified as safe exploration~\cite{safe_exploration}, focuses on developing techniques to explore the environment in a safe manner.

As a case study, we use the \textsc{RTA}\xspace approach for decomposing the problem of optimized exploration from the problem of providing safety guarantee for a robot working in a previously unknown environment.
In the obstacle avoidance property considered in the Section 5.1 in the paper, the motion planner was aware of the static obstacles in the system.

To design the \textsc{RTA}\xspace module to safely explore unknown environments, we need to (1) Design \textsc{RTA}\xspace components $\ensuremath{N_{ac}}$, $\ensuremath{N_{sc}}$ and $\phi_{safe}$, (2) Design the switching condition $\mathtt{ttf}_{2 \ensuremath{\Delta}}$ for switching from AC to SC, and (3) Programming the switching from SC to AC and choosing an appropriate $\ensuremath{\Delta}$ and $\phi_{safer}$.

\textbf{\textit{Design \textsc{RTA}\xspace components.}} In this experiment, $\ensuremath{N_{ac}}$ is a motion planner designed to explore the environment in an optimal way with minimum number of steps and the $\ensuremath{N_{sc}}$ is responsible to bring the system to an \textit{a-priori} known part of the environment.
$\phi_{safe}$ is the entire state space outside the obstacles.

\textbf{\textit{Design $\mathtt{ttf}_{2 \ensuremath{\Delta}}$ for switching from AC to SC.}} If the environment was known \textit{a-priori} we could have used the reachability based technique proposed in Section 5.1 in the paper. However, in the absence of full knowledge of the environment, we approximate $\mathtt{ttf}_{2 \ensuremath{\Delta}} := \{{s}: {s} \in \mathcal{S} \text { s.t. } {s} + v_{max} \cdot 2 \cdot \ensuremath{\Delta} \notin \phi_{safe}\}$ where $v_{max}$ is the maximum velocity attainable by the quadrotor in $x, y,$ or $ z$ direction. Intuitively, it checks if a state would leave $\phi_{safe}$ in $2 \ensuremath{\Delta}$ if it was moving with its highest velocity. This function is more conservative compared to $\mathtt{ttf}_{2 \ensuremath{\Delta}}$ proposed in Section 5.1 computed using reachability. However, this is fast to compute and can be computed on the fly, making it particularly attractive to be used in partially observable environment.

\textbf{\textit{Programming switching from SC to AC.}} Since the environment is unknown, we have to be conservative about our set $\phi_{safer}$. In our experiments, $\phi_{safer}$ is a predefined known area of the state space. The switching from SC to AC occurs at the boundary of the set $\SR{\phi_{safer}}{\ensuremath{\Delta}}$. Similar to Section 5.1, $\ensuremath{\Delta}$ should be chosen to avoid overly-conservative $\mathtt{ttf}_{2 \ensuremath{\Delta}}$ and $\SR{\phi_{safer}}{\ensuremath{\Delta}}$.

\textbf{\textit{Experimental results. }} We used our \textsc{RTA}\xspace module to safely explore an environment(Figure~\ref{Fig:safe_exp}) by avoiding collision with the surrounding wall in gray whose location is unknown \textit{a-priori}.
$\phi_{safe}$ is the entire workspace contained within the gray wall, $\SR{\phi_{safer}}{\ensuremath{\Delta}}$ is the green square at the center of the workspace.
Additionally, $\ensuremath{\Delta}$ is chosen such that $\SR{\phi_{safe}}{\ensuremath{\Delta}}$ is the square with the black boundary and $\SR{\phi_{safe}}{2\ensuremath{\Delta}}$ is the square with the dashed black boundary.

\begin{wrapfigure}{l}{0.6\columnwidth}

	\centering
	\includegraphics[scale=0.25]{figures/safe_exp}
	\caption{Safe exploration using \textsc{RTA}\xspace module}
	\label{Fig:safe_exp}
\end{wrapfigure}

In our experiment, the exploring motion planner generates goal points $g_1-g_{10}$ (black crosses in~\ref{Fig:safe_exp}) for the drone to traverse, sequentially.
For each goal point, $g_i$, $\ensuremath{N_{ac}}$ plans a path from the current position of the quadcopter, $\mathbf{x}_t$ to the $g_i$.
However, during exploration when $g_i$ satisfies $\mathtt{ttf}_{2 \ensuremath{\Delta}}$, our \textsc{RTA}\xspace module detects the wall at runtime, switches to {\sc SC}\xspace (shown by green dot in Figure~\ref{Fig:safe_exp}) when the trajectory leaves $\SR{\phi_{safe}}{2\ensuremath{\Delta}}$ while still inside $\SR{\phi_{safe}}{\ensuremath{\Delta}}$. $\ensuremath{N_{sc}}$ brings the trajectory back to $\phi_{safer}$ (shown by the orange trajectory). Once inside $\SR{\phi_{safer}}{\ensuremath{\Delta}}$, the {\sc DM}\xspace hands back control to the $\ensuremath{N_{ac}}$ (shown by red dot) and the exploration process begins again.

\section{Operational Semantics of an \textsc{RTA}\xspace Module}
\label{sec:semantics}
In \text{\small \textsc{Soter}}\xspace, a complex system is designed as a composition of \textsc{RTA}\xspace modules.
An \textsc{RTA}\xspace system is a set of \textit{composable} \textsc{RTA}\xspace modules.
A set of modules $S = \{M_0, M_1, \dots, M_n\}$ are composable if:
\begin{mylist}
	\item The nodes in all modules are disjoint, if $\ensuremath{N_{ac}}^i$, $\ensuremath{N_{sc}}^i$, and $\ensuremath{N_{dm}}^i$ represent the {\sc AC}\xspace, {\sc SC}\xspace and {\sc DM}\xspace nodes of a module $M_i$ then, for all $i, j$ s.t. $i \neq j$, $\{\ensuremath{N_{ac}}^i, \ensuremath{N_{sc}}^i, \ensuremath{N_{dm}}^i\} \cap \{\ensuremath{N_{ac}}^j, \ensuremath{N_{sc}}^j, \ensuremath{N_{dm}}^j\} = \emptyset$.
	\item The outputs of all modules are disjoint, for all $i, j$ s.t. $i \neq j$, $\Outputs{M_i} \cap \Outputs{M_j} = \emptyset$.
\end{mylist}

Note that only constraint for composition is that the outputs (no constraints on inputs) must be disjoint as described by traditional compositional frameworks like I/O Automata and Reactive Modules~\cite{alur1999reactive,lynch1988introduction}.

\noindent
\textit{\textbf{Composition.}}
If \textsc{RTA}\xspace modules $\ensuremath{P}$ and $\ensuremath{Q}$ are composable then their composition $\ensuremath{P} \parallel \ensuremath{Q}$ is an \textsc{RTA}\xspace system consisting of the two modules $\{ \ensuremath{P}, \ensuremath{Q}\}$.
Also, composition of two \textsc{RTA}\xspace systems $S1$ and $S2$ is an \textsc{RTA}\xspace system $S1 \cup S2$, if all modules in $S1 \cup S2$ are composable.

\vspace{0.2cm}
\begin{thm}[\textbf{Compositional \textsc{RTA}\xspace System}]
	\textit{Let $S = \{M_0, \dots M_n\}$ be an \textsc{RTA}\xspace system. If for all $i$, $M_i$ is a well-formed \textsc{RTA}\xspace module satisfying the safety invariant $\phi^i_{Inv}$ then, $S$ satisfies the invariant $\bigwedge_i \phi^i_{Inv}$.}

	\label{thm:comp}
\end{thm}
\vspace{0.2cm}
\textit{Proof.}
Note that this theorem simply follows from the fact that composition just restricts the environment.
Since we are guaranteed output disjointness during composition, composition of two modules is guaranteed to be language intersection.
The proof for such composition theorem is described in details in ~\cite{alur1999reactive,lynch1988introduction}.

Theorem~\ref{thm:comp} plays an important role in building the reliable software stack in Figure~\ref{fig:casestudy}c.
Each \textsc{RTA}\xspace module individually satisfies the respective safety invariant and their composition helps establish the system-level specification.

We use $\ensuremath{\mathtt{dom}}(X)$ to refer to the domain of map $X$ and $\ensuremath{\mathtt{codom}}(X)$ to refer to the codomain of $X$.
Given an \textsc{RTA}\xspace system $S = \{M_0, \dots, M_n\}$, its attributes (used for defining the operational semantics) can be inferred as follows:

\begin{mylist}
	\item $\ensuremath{{ACNodes}} \in \ensuremath{\mathcal{N}} \rightarrow \ensuremath{\mathcal{N}}$ is a map that binds a {\sc DM}\xspace node $n$ to the particular {\sc AC}\xspace node $\ensuremath{{ACNodes}}[n]$ it controls, i.e., if $M_i \in S$ then $(\ensuremath{N_{dm}}^i, \ensuremath{N_{ac}}^i) \in \ensuremath{{ACNodes}}$.
	\item $\ensuremath{{SCNodes}} \in \ensuremath{\mathcal{N}} \rightarrow \ensuremath{\mathcal{N}}$ is a map that binds a {\sc DM}\xspace node $n$ to the particular {\sc SC}\xspace node $\ensuremath{{SCNodes}}[n]$ it controls, i.e., if $M_i \in S$ then $(\ensuremath{N_{dm}}^i, \ensuremath{N_{sc}}^i) \in \ensuremath{{SCNodes}}$.
	\item $\ensuremath{{Nodes}} \subseteq \ensuremath{\mathcal{N}}$ represents the set of all nodes in the \textsc{RTA}\xspace system, $\ensuremath{{Nodes}} = \ensuremath{\mathtt{dom}}(\ensuremath{{ACNodes}}) \cup \ensuremath{\mathtt{codom}}(\ensuremath{{ACNodes}}) \cup \ensuremath{\mathtt{codom}}(\ensuremath{{SCNodes}})$.
	\item $\ensuremath{OS} \subseteq \ensuremath{\mathcal{T}}$ represents the set of outputs of the \textsc{RTA}\xspace system, $\ensuremath{OS} = \bigcup_{n \in \ensuremath{{Nodes}}} \Outputs{n}$.
	\item $\ensuremath{IS} \subseteq \ensuremath{\mathcal{T}}$ represents the set of inputs of the \textsc{RTA}\xspace system (inputs from the environment), $\ensuremath{IS} = \bigcup_{n \in \ensuremath{{Nodes}}} \Inputs{n} \setminus \ensuremath{OS}$.
	\item $\ensuremath{CS}$ represents the calendar or time-table of the \textsc{RTA}\xspace system, $\ensuremath{CS} = \bigcup_{n \in \ensuremath{{Nodes}}} \Calendar{n}$.
\end{mylist}

We refer to the attributes of a \textsc{RTA}\xspace system $S$ as $\ensuremath{{ACNodes}}(S)$, $\ensuremath{{SCNodes}}(S)$, $\AllNodes{S}$, $\MOutputs{S}$, $\MInputs{S}$, and $\MCalendar{S}$ respectively.

We next present the semantics of an \textsc{RTA}\xspace system.
Note that the semantics of an \textsc{RTA}\xspace module is the semantics of an \textsc{RTA}\xspace system where the system is a singleton set.
We use the timeout-based discrete event simulation model~\cite{dutertre2004modeling} for modeling the semantics of an \textsc{RTA}\xspace system.
The calendar $\ensuremath{CS}$ stores the future times at which nodes in the \textsc{RTA}\xspace system must step.
Using a variable $\ensuremath{ct}$ to store the current time and $\ensuremath{FN}$ to store the enabled nodes, we can model the real-time system as a discrete transition system.

\noindent
\textbf{Configuration.}
A configuration of an \textsc{RTA}\xspace system is a tuple $(\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics})$ where:
\begin{mylist}
	\item $\ensuremath{L} \in \ensuremath{{Nodes}} \rightarrow \ensuremath{\mathcal{L}}$ represents a map from a node to the local state of that node.
	\item $\ensuremath{OE} \in \ensuremath{\mathcal{N}} \rightarrow \mathbb{B}$ represents a map from a node to a boolean value indicating whether the output of the node is enabled or disabled. This is used for deciding whether {\sc AC}\xspace or {\sc SC}\xspace should be in control. The domain of $\ensuremath{OE}$ is $\ensuremath{\mathtt{codom}}(\ensuremath{{ACNodes}}) \cup \ensuremath{\mathtt{codom}}(\ensuremath{{SCNodes}})$.
	\item $\ensuremath{ct} \in \mathbb{R}$ represents the current time.
	\item $\ensuremath{FN} \subseteq \ensuremath{\mathcal{N}}$ represents the set of nodes that are remaining to be fired at time $\ensuremath{ct}$.
	\item $\ensuremath{Topics} \in \ensuremath{\mathcal{T}} \rightarrow \ensuremath{\mathcal{V}}$ is a map from a topic name to the value stored at that topic, it represents the globally visible topics.
	If $X \subseteq \ensuremath{\mathcal{T}}$ then $\ensuremath{Topics}[X]$ represents a map from each $x \in X$ to $\ensuremath{Topics}[x]$.
\end{mylist}

The initial configuration of any \textsc{RTA}\xspace system is represented as $(\ensuremath{L}_0, \ensuremath{OE}_0, \ensuremath{ct}_0, \ensuremath{FN}_0, \ensuremath{Topics}_0)$ where:
$\ensuremath{L}_0$ maps each node in its domain to default local state value $l_0$ if the node is {\sc AC}\xspace or {\sc SC}\xspace, otherwise, $mode = {\sc SC}\xspace$ for the {\sc DM}\xspace node, $\ensuremath{OE}_0$ maps each {\sc SC}\xspace node to {\tt true} and {\sc AC}\xspace node to {\tt false} (this is to ensure that each \textsc{RTA}\xspace module starts in {\sc SC}\xspace mode), $\ensuremath{ct}_0 = 0$,  $\ensuremath{FN}_0 = \emptyset$, and $\ensuremath{Topics}_0$ maps each topic name to its default value $v \in \ensuremath{\mathcal{V}}$.

We represent the operational semantics of a \textsc{RTA}\xspace system as a transition relation over its configurations (Figure~\ref{fig:semantics}).

\begin{figure}[th]
	\vspace{-0.3cm}
	\scriptsize
	\begin{mathpar}
		{\text{\small ITE(x, y, z) represents if x then y else z}}

		\inferrule*[lab=(\textbf{\textsc{Environment-Input}})]
		{\ensuremath{e} \in \ensuremath{IS} \\ v \in \ensuremath{\mathcal{V}}}
		{(\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics}) \rightarrow (\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics}[\ensuremath{e} \mapsto v])}

		\inferrule*[lab=(\textbf{\textsc{Discrete-Time-Progress-Step}})]
		{\ensuremath{FN} = \emptyset^{\cond{dt1}} \, \ensuremath{ct}' = \min(\{t \, | \, (x, t) \in \ensuremath{CS}, t > \ensuremath{ct}\})^{\cond{dt2}} \\\\ \ensuremath{FN}' = \{n \, | \, (n, \ensuremath{ct}') \in \ensuremath{CS}\}^{\cond{dt3}}}
		{(\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics}) \rightarrow (\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}', \ensuremath{FN}', \ensuremath{Topics})}

		\inferrule*[lab=(\textbf{\textsc{{\sc DM}\xspace-Step}})]
		{dm \in \ensuremath{FN} \\ \ensuremath{FN}' = \ensuremath{FN}\setminus\{dm\} \\ dm \in \ensuremath{\mathtt{dom}}(\ensuremath{{ACNodes}}) \\ (l, \{(\ensuremath{{\tt STATE}}, s_t)\}, l', \emptyset) \in \Transitions{dm} \\ ac = \ensuremath{{ACNodes}}[dm] \\ sc = \ensuremath{{SCNodes}}[dm] \\ \ensuremath{{\tt \mathbf{ITE}}}(l' = {\sc AC}\xspace, en = \mathtt{true}, en = \mathtt{false})^{\cond{dm1}} }
		{(\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics}) \rightarrow \\\\
			(\ensuremath{L}[dm \mapsto l'], \ensuremath{OE}[ac \mapsto en, sc \mapsto \neg en]^{\cond{dm2}}, \ensuremath{ct}, \ensuremath{FN}' , \ensuremath{Topics})}

		\inferrule*[lab=(\textbf{\textsc{{\sc AC}\xspace-or-{\sc SC}\xspace-Step}})]
		{n \in \ensuremath{FN}\\ \ensuremath{FN}' = \ensuremath{FN}  \setminus \{n\}\\ n \not \in \ensuremath{\mathtt{dom}}(\ensuremath{{ACNodes}})\\ in = \ensuremath{Topics}[\Inputs{n}]\\ (l, in, l', out) \in \Transitions{n}
		\\ \ensuremath{{\tt \mathbf{ITE}}}(OE[n], \ensuremath{Topics}' = out \cup \ensuremath{Topics}[\ensuremath{\mathcal{T}}\setminus\ensuremath{\mathtt{dom}}(out)], \ensuremath{Topics}' = \ensuremath{Topics})^{\cond{n1}}}
		{(\ensuremath{L}, \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}, \ensuremath{Topics}) \rightarrow (\ensuremath{L}[n \mapsto l'], \ensuremath{OE}, \ensuremath{ct}, \ensuremath{FN}', \ensuremath{Topics}')}

	\end{mathpar}
	\vspace{-0.9cm}
	\caption{Semantics of an \textsc{RTA}\xspace System}
	\label{fig:semantics}
	\vspace{-0.2cm}
\end{figure}

There are two types of transitions: \point{1} discrete transitions that are instantaneous and hence does not change the current time, and \point{2} time-progress transitions that advance time when no discrete transition is enabled.
\textsc{{\sc DM}\xspace-Step} and \textsc{{\sc AC}\xspace-or-{\sc SC}\xspace-Step} are the discrete transitions of the system.
\textsc{Environment-Input} transitions are triggered by the environment and can happen at any time.
It updates any of the input topics $e \in \ensuremath{IS}$ of the module to $(e, v)$.
\textsc{Discrete-Time-Progress-Step} represents the time-progress transitions that can be executed when no discrete transitions are enabled \cond{dt1}.
It updates $\ensuremath{ct}$ to the next time at which a discrete transition must be executed \cond{dt2}.
$\ensuremath{FN}$ is updated to the set of nodes that are enabled and must be executed \cond{dt3} at the current time.
\textsc{{\sc DM}\xspace-Step} represents the transition of any of the {\sc DM}\xspace nodes in the module. The important operation performed by this transition is to enable or disable the outputs of the {\sc AC}\xspace and {\sc SC}\xspace node \cond{dm2} based on its current \textit{mode} \cond{dm1}.
Finally, \textsc{{\sc AC}\xspace-or-{\sc SC}\xspace-Step} represents the step of any {\sc AC}\xspace or {\sc SC}\xspace node in the module. Note that the node updates the output topics only if its output is enabled (based on $\ensuremath{OE}(n)$ \cond{n1}).

\noindent
\textbf{Reachability.}
Note that the state space $\mathcal{S}$ of an \textsc{RTA}\xspace system is the set of all possible configurations.
The set of all possible reachable states of an \textsc{RTA}\xspace system is a set of configurations that are reachable from the initial configuration using the transition system described in Figure~\ref{fig:semantics}.
Since the environment transitions are nondeterministic, potentially many states are reachable even if the \textsc{RTA}\xspace modules are all deterministic.

Let $\ensuremath{Reach}_{M}({s}, \ensuremath{N_{sc}}, t) \subseteq \mathcal{S}$ represent the set of all states of the \textsc{RTA}\xspace system $S$ reachable in time $[0,t]$ starting from the state ${s}$, using only the controller {\sc SC}\xspace node $\ensuremath{N_{sc}}$ of the \textsc{RTA}\xspace module $M \in S$.
In other words, instead of switching control between {\sc SC}\xspace and {\sc AC}\xspace of the \textsc{RTA}\xspace module $M$, the {\sc DM}\xspace always keeps {\sc SC}\xspace node in control.
$\ensuremath{Reach}_{M}({s}, *, t) \subseteq \mathcal{S}$ represents the set of all states of the \textsc{RTA}\xspace system $S$ reachable in time $[0,t]$ starting from the state ${s}$, using only a completely nondeterministic module instead of $M \in S$.
In other words, instead of module $M$, a module that generates nondeterministic values on the output topics of $M$ is used.
The notation $\ensuremath{Reach}$ is naturally extended to a set of states:
$\ensuremath{Reach}_{M}(\psi, x, t) = \bigcup_{{s}\in\psi}\ensuremath{Reach}_{M}({s},x,t)$ is the set of all states reachable in time $[0,t]$ when starting from a state ${s}\in\psi$ using $x$.
Note that, {\small $\ensuremath{Reach}_{M}(\psi,\ensuremath{N_{sc}},t) \subseteq \ensuremath{Reach}_{M}(\psi,*,t) $}.

We note that the definition of  {\sc DM}\xspace for an \textsc{RTA}\xspace module $M$ is sensitive to the choice of the environment for $M$. Consequently, every attribute of $M$ (such as well-formedness) depends on the context in which $M$ resides. We implicitly assume that all definitions of $M$ are based on a completely nondeterministic context. All results hold for this interpretation, but they also hold for any more constrained environment.

\section{Runtime Assurance Protected Robotics System}

\label{sec:trustedsoftware}

In this section, we describe how the \textsc{RTA}\xspace module (Section~\ref{sec:simplex}) can be used to guarantee obstacle avoidance and battery safety in the presence of untrusted components.

\input{safecontrol}

\input{batterysafety}
\subsection{\textsc{RTA}\xspace-Protected Safe Motion Primitives}
A drone navigates in the 3D space by tracking trajectories between waypoints computed by the motion planner.
Given the next waypoint, an appropriate motion primitive is used to track the reference trajectory.
Informally, a motion primitive consists of a pre-computed control law (sequence of control actions) that regulates the state of the drone as a function of time.
For our experiments in Figure~\ref{fig:controllerexp}, we used the motion primitives provided by the PX4 autopilot~\cite{px4} as our advanced controller and found that it can lead to failures or collision.

To achieve \textsc{RTA}\xspace-protected motion primitive, there are three essential steps: (1) Design of the safe controller $\ensuremath{N_{sc}}$; (2) Designing the $\mathtt{ttf}_{2\ensuremath{\Delta}}$ function that controls switching from the {\sc AC}\xspace to {\sc SC}\xspace for the motion primitive; (3) Programming the switching from {\sc SC}\xspace to {\sc AC}\xspace and choosing an appropriate $\ensuremath{\Delta}$ and $\phi_{safer}$ so that the system is not too conservative.

When designing the $\ensuremath{N_{sc}}$, it must satisfy the Property~\cond{P2}, where $\phi_{safe}$ is the region not occupied by any obstacle.
Techniques from control theory, like \textit{reachability}~\cite{Reachability} can be used for designing $\ensuremath{N_{sc}}$.
We use the FaSTrack~\cite{herbert2017fastrack} tool for generating a correct-by-construction controller for the drone such that it satisfies all the properties required for a $\ensuremath{N_{sc}}$.

To design the switching condition from {\sc AC}\xspace to {\sc SC}\xspace, we need to compute the $\mathtt{ttf}$ function that checks $\ensuremath{Reach}(s_t,*,2\ensuremath{\Delta}) \not\subseteq\phi_{safe}$ (Figure~\ref{fig:dmlogic}) where $s_t$ is the current state.
Consider the 2D representation of the workspace (Figure~\ref{fig:casestudy}) in Figure~\ref{fig:results}b.
The obstacles (shown in grey) represent the $\phi_{unsafe}$ region and any region outside is $\phi_{safe}$.
Note that, $\ensuremath{N_{sc}}$ can guarantee safety for all locations in $\phi_{safe}$ \cond{P2}.
We can use the level set toolbox~\cite{Reachability}
to compute the backward reachable set from $\phi_{safe}$ in $2\ensuremath{\Delta}$~(shown in yellow), i.e., the set of states from where the drone can leave $\phi_{safe}$ (collide with obstacle) in $2\ensuremath{\Delta}$.
In order to maximize the performance of the system, the \textsc{RTA}\xspace module must switch from SC to AC after the system has recovered.
In our experiments, we choose $\phi_{safer} = \SR{\phi_{safe}}{2\ensuremath{\Delta}}$~(shown in green).
$\ensuremath{N_{sc}}$ is designed such that given $\phi_{safer}$, Property \cond{P2b} holds.
{\sc DM}\xspace transfers control to {\sc AC}\xspace when it detects that the drone is in $\phi_{safer}$, which is the backward reachable set from $\phi_{safe}$ in $2\ensuremath{\Delta}$ time.

Choosing the period $\ensuremath{\Delta}$ is an important design decision.
Choosing a large $\ensuremath{\Delta}$ can lead to overly-conservative $\mathtt{ttf}_{2\ensuremath{\Delta}}({s}_t, \phi_{safe})$ and $\phi_{safer}$.
In other words, a large $\ensuremath{\Delta}$ pushes the switching boundaries further away from the obstacle.
In which case, a large part of the workspace is covered by red or yellow region where {\sc SC}\xspace (conservative controller) is in control.

We implemented the safe motion primitive as a \textsc{RTA}\xspace module using the components described above.
Figure~\ref{fig:results}a presents one of the interesting trajectories where the {\sc SC}\xspace takes control multiple times and ensures the overall correctness of the mission.
The green tube inside the yellow tube represents the $\phi_{safer}$ region.
The red dots represent the points where the {\sc DM}\xspace switches control to {\sc SC}\xspace and the green dots represent the points where the {\sc DM}\xspace returns control back to the {\sc AC}\xspace for optimizing performance.
The average time taken by the drone to go from $g_1$ to $g_4$ is 10 secs when only the unsafe $\ensuremath{N_{ac}}$ is in control (can lead to collisions), it is 14 secs when using the \textsc{RTA}\xspace protected safe motion primitive, and 24 secs when only using the safe controller.
Hence, using \textsc{RTA}\xspace provides a ``safe'' middle ground without sacrificing performance too much.

Figure~\ref{fig:results}b presents the 2D representation of our workspace in Gazebo (Figure~\ref{fig:casestudy}a).
The dotted lines represent one of the reference trajectories of the drone during the surveillance mission.
The trajectory in solid shows the trajectory of the drone when using the \textsc{RTA}\xspace-protected software stack consisting of the safe motion primitive.
At N1 and N2, the $\ensuremath{N_{sc}}$ takes control and pushes the drone back into $\phi_{safer}$ (green); and returns control back to $\ensuremath{N_{ac}}$.
We observe that the $\ensuremath{N_{ac}}$ is in control for the most part of the surveillance mission even in cases when the drone deviates from the reference trajectory (N3) but is still safe.

redpajama_set_name: RedPajamaArXiv