ITR/SY: Verification Tools for Autonomous and Embedded Systems

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

This research project is developing a new generation of formal verification tools that can be integrated into design environments for the complex, high-assurance embedded and autonomous systems of today and of the future. Such systems are increasingly distributed, complex, and dynamic; they must operate with a high degree of autonomy and survivability in diverse and unpredictable environments. This project will focus on the development of new verification methods and tools to provide a rigorous means for checking the integrity and correctness of designs for these systems before they are deployed. The project has two broad research thrusts: 1. Verifying System Integrity. System integrity refers to correctness with respect to the interactions among the distributed software and hardware components. Systems must satisfy synchronization, resource, and real-time constraints imposed by the implementation architecture and application requirements. This project will extend automated verification methods that have been successful in hardware and protocol applications to their use with embedded and autonomous systems. 2. Modeling the Environment. Embedded and autonomous systems must interact in complex ways with physical systems and adverse environments. It is thus essential to capture correctly and effectively the continuous dynamics, feedback loops, and unpredictable features of the environment in the models used for formal verification. This project will draw on recent developments in hybrid system verification to integrate continuous state dynamics with discrete-state models used in formal verification.