ITR/SY: Verification Tools for Autonomous and Embedded Systems

该研究项目正在开发新一代的正式验证工具，这些工具可以集成到当今和未来复杂的、高保证的嵌入式和自主系统的设计环境中。这些系统越来越分散、复杂和动态；它们必须在多样化和不可预测的环境中具有高度的自主性和生存能力。该项目将侧重于开发新的验证方法和工具，以提供在部署这些系统之前检查其设计的完整性和正确性的严格方法。该项目有两大研究重点：1。验证系统完整性。系统完整性是指分布式软件和硬件组件之间相互作用的正确性。系统必须满足实现体系结构和应用程序需求所施加的同步、资源和实时约束。该项目将扩展在硬件和协议应用中成功的自动验证方法，以用于嵌入式和自治系统。2. 环境建模。嵌入式和自治系统必须以复杂的方式与物理系统和不利环境相互作用。因此，在用于正式验证的模型中，正确有效地捕获连续动态、反馈循环和环境的不可预测特征是必不可少的。该项目将借鉴混合系统验证的最新发展，将连续状态动力学与形式验证中使用的离散状态模型集成在一起。

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.