Safe Autonomy

Validation & Verification of Robotic Systems

From robots working alongside humans every day to the one-of-a-kind rovers sent to Mars once in a while (at least for now!), it is crucial to ensure correct and safe operation of robotic systems. The need for integrating several software modules (e.g., for perception, high-level decision-making, and control) for complex robotic systems exacerbates the problem because, if it is not done with care, unexpected interactions can lead to system-level failures after integration. Testing each and every scenario and interaction the system can go trough is not feasible, therefore more systematic means for verifying safety and correctness are needed. The goal of V&V research is to provide certificates on the correct and safe operation of the system given a set of assumptions on the system’s environment and the implementation platform.

The problems Michigan faculty and students work on include:

• Specification languages and modeling formalisms: How to describe correct behavior of different types of robotic systems in a way amenable to analysis?
• Verification and formal methods for robotics: Algorithmic techniques to prove safety and correctness of the system or to find corner cases that can lead to problems.
• Fault-tolerance and monitoring: How to do health-monitoring and prognostics to improve the self-awareness of robotic systems at run-time? How to locate and mitigate faults in a timely manner?
• Correct-by-construction control synthesis: Algorithmic techniques to automate the design of control and decision-making modules (software designed by another software!) in a way that given system models and requirements, the resulting software modules are guaranteed to enforce the specifications.