Formal Analysis of Perception Errors and Their System-level Effects

We are considering a system to produce alerts for runway incursions enabling safe landing of airplanes.
The system is implemented as an ML based object detector, followed by downstream conventional modules for tracking and alerting.

Goal: Investigate how imperfect ML perception affects system behavior guided by formal specifications.

Broad outline of steps:
1. Identify semantic conditions associated with perception errors (false and missed detections).
2. Formally guide system testing: Create diagnostic specifications (temporal and semantic) and test the detector–tracker–alert pipeline wrt the specifications.
3. Characterize and investigate system failures: Analyze violation traces and execution logs to mine recurring failure patterns and determine how perception errors propagate to system-level behavior.
4. The project will also investigate model-checking methods (time-permitting) to identify and characterize failures.

**Eligible Applicants:** Student
**Academic Level:** Undergraduate Senior, Graduate Master's, Graduate Doctoral, Post Doctoral
**Activity Type:** In-person
**Citizenship:** US Citizen Only
**Type:** Internships