ITR/SY: Verification Tools for Autonomous and Embedded Systems

ITR/SY：自主和嵌入式系统的验证工具

• 批准号: 0121547
• 负责人: Edmund Clarke
• 金额: $ 100万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-09-01 至 2005-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0121547&HistoricalAwards=false
• 关键词: ITR; SY; Verification; Tools; Autonomous

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.

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