[HTML][HTML] Towards a framework for certification of reliable autonomous systems

M Fisher, V Mascardi, KY Rozier, BH Schlingloff… - Autonomous Agents and …, 2021 - Springer
A computational system is called autonomous if it is able to make its own decisions, or take
its own actions, without human supervision or control. The capability and spread of such …

Embedding online runtime verification for fault disambiguation on robonaut2

B Kempa, P Zhang, PH Jones, J Zambreno… - … Conference on Formal …, 2020 - Springer
Abstract Robonaut2 (R2) is a humanoid robot onboard the International Space Station (ISS),
performing specialized tasks in collaboration with astronauts. After deployment, R2 …

Runtime verification triggers real-time, autonomous fault recovery on the CySat-I

A Aurandt, PH Jones, KY Rozier - NASA Formal Methods Symposium, 2022 - Springer
CubeSats are low-cost platforms that are popular for conducting spaceborne experiments,
however they are known to have high failure rates (∼ 25% failure rate). In order to improve …

[HTML][HTML] R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware …

C Johannsen, P Jones, B Kempa, KY Rozier… - … on Computer Aided …, 2023 - Springer
R2U2 is a modular runtime verification framework capable of monitoring sets of
specifications in real time and in resource-constrained environments. Such environments …

RTAMT–Runtime Robustness Monitors with Application to CPS and Robotics

T Yamaguchi, B Hoxha, D Ničković - International Journal on Software …, 2024 - Springer
In this paper, we present the Real-Time Analog Monitoring Tool (RTAMT), a tool for
quantitative monitoring of Signal Temporal Logic (STL) specifications. The library …

Adding a verification view for an autonomous real-time system architecture

JB Dabney, JM Badger, P Rajagopal - AIAA SciTech 2021 Forum, 2021 - arc.aiaa.org
View Video Presentation: https://doi. org/10.2514/6.2021-0566. vid Spacecraft software
systems continue to increase in complexity and must frequently operate autonomously for …

Elucidation and analysis of specification patterns in aerospace system telemetry

Z Luppen, M Jacks, N Baughman, M Stilic… - NASA Formal Methods …, 2022 - Springer
Experimental aerospace projects often require flight vehicle platforms for testing, such as
high-altitude balloons, sounding rockets, unmanned aerial systems (UAS), and CubeSats …

Programmable logic controllers past linear temporal logic for monitoring applications in industrial control systems

X Mao, X Li, Y Huang, J Shi… - IEEE Transactions on …, 2021 - ieeexplore.ieee.org
Programmable logic controllers (PLC), which are widely applied in modern industrial control
systems (ICS), work as the controller of sensors and actuators in ICS. These systems require …

Mission-time ltl (mltl) formula validation via regular expressions

J Elwing, L Gamboa-Guzman, J Sorkin… - … on Integrated Formal …, 2023 - Springer
Abstract Mission-time Linear Temporal Logic (MLTL) represents the most practical fragment
of Metric Temporal Logic; MLTL resembles the popular logic Linear Temporal Logic (LTL) …

Integrating runtime verification into an automated uas traffic management system

M Cauwels, A Hammer, B Hertz, PH Jones… - … Conference on Software …, 2020 - Springer
Abstract Unmanned Aerial Systems (UAS) are quickly integrating into the National Air Space
(NAS). With the number of registered small (under 55 pounds) UAS in the USA alone at over …