
@conference {KemZha20A,
	title = {Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2},
	booktitle = {Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)},
	year = {2020},
	month = {September},
	abstract = {Robonaut2 (R2) is a humanoid robot onboard the International Space Station (ISS), performing specialized tasks in collaboration with astronauts. After deployment, R2 developed an unexpected emergent behavior. R2{\textquoteright}s inability to distinguish between knee-joint faults (e.g., due to sensor drift versus violated environmental assumptions) began triggering mid-task, safety-preserving freezes-in-place in the confined space of the ISS, preventing further motion until a ground-control operator determines the root-cause and initiates proper corrective action. Runtime verification (RV) algorithms can efficiently disambiguate the temporal signatures of different faults in real-time. However, no previous RV engine can operate within the limited available resources and specialized platform constraints of R2{\textquoteright}s hardware architecture. An attempt to deploy the only runtime verification engine designed for embedded flight systems, R2U2, failed due to resource constraints. We present a significant redesign of the core R2U2 algorithms to adapt to severe resource and certification constraints and prove their correctness, time complexity, and space requirements. We further define optimizations enabled by our new algorithms and implement the new version of R2U2. We encode specifications describing real-life faults occurring onboard Robonaut2 using MLTL and detail our process of specification debugging, validation, and refinement. We deploy this new version of R2U2 on Robonaut2, demonstrating successful real-time fault disambiguation and mitigation triggering of R2{\textquoteright}s knee-joint faults without false positives.},
	author = {Brian Kempa and Pei Zhang and Phillip Jones and Joseph Zambreno and Kristin Yvonne Rozier}
}
@conference {ZhaZam17A,
	title = {An Embedded Scalable Linear Model Predictive Hardware-based Controller using ADMM},
	booktitle = {Proceedings of the International Conference on Application-specific Systems, Architectures and Processors (ASAP)},
	year = {2017},
	month = {July},
	abstract = {Model predictive control (MPC) is a popular advanced model-based control algorithm for controlling systems that must respect a set of system constraints (e.g. actuator force limitations). However, the computing requirements of MPC limits the suitability of deploying its software implementation into embedded controllers requiring high update rates. This paper presents a scalable embedded MPC controller implemented on a field-programmable gate array (FPGA) coupled with an on-chip ARM processor. Our architecture implements an Alternating Direction Method of Multipliers (ADMM) approach for computing MPC controller commands. All computations are performed using floating-point arithmetic. We introduce a software/hardware (SW/HW) co-design methodology, for which the ARM software can configure on-chip Block RAM to allow users to 1) configure the MPC controller for a wide range of plants, and 2) update at runtime the desired trajectory to track. Our hardware architecture has the flexibility to compromise between the amount of hardware resources used (regarding Block RAMs and DSPs) and the controller computing speed. For example, this flexibility gives the ability to control plants modeled by a large number of decision variables (i.e. a plant model using many Block RAMs) with a small number of computing resources (i.e. DSPs) at the cost of increased computing time. The hardware controller is verified using a Plant-on-Chip (PoC), which is configured to emulate a mass-spring system in real-time. A major driving goal of this work is to architect an SW/HW platform that brings FPGAs a step closer to being widely adopted by advanced control algorithm designers for deploying their algorithms into embedded systems.},
	author = {Pei Zhang and Joseph Zambreno and Phillip Jones}
}
