SHF: Small: Scalable Formal Verification of ANN controlled Cyber-Physical Systems
Scott DeLoach
Lead PI:
Scott DeLoach
Abstract

Artificial Neural Networks (ANN) are increasingly being employed to monitor and control Cyber-Physical Systems (CPS), as in autonomous ground and aerial vehicles. With increasing complexity and safety criticality of these systems, formal-verification techniques that provide rigorous guarantees are urgently needed. The broad goal of the research is to develop novel algorithms and software tools for formal verification of ANN-controlled CPS (ANN-CPS). One of the main challenges of existing techniques is their scalability to large number of neurons and complex physical dynamics.

Using the novel concept of Interval Neural Networks, coupled with ideas from formal methods such as counter-example guided abstraction refinement and approximate bisimulation, the project investigates scalable formal verification techniques for ANN-CPS. The results of the project will enable rigorous analysis of complex ANN-CPS possible, thereby enhancing their reliability in applications such as autonomous driving. Further, the PI is engaged in course development, mentorship of undergraduate and graduate students, and outreach activities for K-12 students, with the broader aim of motivating and building the workforce for formal analysis of cyber-physical systems.

Performance Period: 10/01/2020 - 09/30/2024
Institution: Kansas State University
Sponsor: National Science Foundation
Award Number: 2008957
Feedback
Feedback
If you experience a bug or would like to see an addition or change on the current page, feel free to leave us a message.
Image CAPTCHA
Enter the characters shown in the image.
This question is for testing whether or not you are a human visitor and to prevent automated spam submissions.