VeriVITAL - The Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory
Research Synopsis: Defects stemming from the interaction of software and physical processes in embedded and cyber-physical systems (CPS) are rampant and are becoming more prevalent as exemplified by frequent product recalls in industries such as automotive, medical devices, and consumer products. To address this challenge to ensure CPS meet the strictest safety, security, and reliability requirements, our research agenda is to develop formal verification techniques and tools for CPS, building on and advancing foundational results in formal methods, control theory, distributed systems, and real-time/embedded systems. For example, one technique we've developed is for verifying safety properties of distributed CPS where arbitrarily many agents participate in a protocol, such as in air traffic control protocols, network protocols, networked control systems, and swarm robotics. This uniform verification technique for parameterized systems verifies systems with arbitrarily many participants, and relies on a small model theorem we developed, which allows for reasoning about arbitrarily large instances using finite instances. Our implementation of this technique in an SMT-based verification software tool (called Passel) allowed us to prove automatically, that in one of NASA's conceptual air traffic control protocols in NextGen, all aircraft maintain a safe separation, regardless of the number of aircraft involved in the protocol. Other techniques we have developed include automated abstractions implemented in our Hyst tool, mixtures of static and dynamic analysis for Simulink/Stateflow models to infer cyber-physical specifications as implemented in our Hynger tool, the first reachability algorithm for hybrid automata that may be implemented with real-time guarantees, among others. Our verification methods have been applied across numerous CPS domains, including automotive, aerospace, power/energy systems, and robotics.