EHS: Graph-Based Refinement Strategies for Hybrid Systems

EHS：混合系统基于图的细化策略

• 批准号: 0411152
• 负责人: Edmund Clarke
• 金额: $ 55万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-09-15 至 2008-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0411152&HistoricalAwards=false
• 关键词: EHS; Graph; Based; Refinement; Strategies

Hybrid systems are characterized by non-trivial interactions between discrete (digital) and continuous (analog) components. A typical example is a digital controller in an analog environment, e.g., a micro-controller in a car or plane. The correct behavior of the system depends critically on the interaction between the controller and its environment. The purpose of this project is to develop algorithms that automatically determine the correctness of such systems using a state exploration technique called Model Checking. Although several methods for hybrid system model checking have been proposed and implemented in research tools, the applications reported in the literature are usually handcrafted examples carefully constructed to illustrate the concepts. The goals of this project are to: (i) develop a new graph-based technique for hybrid system model checking; (ii) develop new methods that combine the power of SAT solvers - which have been successful in hardware verification - with tools for handling continuous variables; and (iii) perform extensive empirical studies to evaluate the relative strengths of several methods for hybrid system verification, including the ones developed in this project, using a set of new extensible benchmark problems (A navigation problem for autonomous vehicles, a leak detection algorithm for pressurized gas pipelines, etc.)

混合系统的特点是离散（数字）和连续（模拟）组件之间的非平凡的相互作用。 典型的例子是模拟环境中的数字控制器，例如，汽车或飞机上的微控制器。系统的正确行为关键取决于控制器与其环境之间的相互作用。这个项目的目的是开发算法，使用称为模型检查的状态探索技术自动确定这些系统的正确性。虽然已经提出了几种混合系统模型检测的方法，并在研究工具中实现，在文献中报道的应用程序通常是手工制作的例子精心构造，以说明的概念。该项目的目标是：（一）为混合系统模型检查开发一种新的基于图形的技术;（二）开发新的方法，将在硬件验证中取得成功的SAT解算器的能力与处理连续变量的工具结合起来;以及（iii）进行广泛的实证研究以评估用于混合系统验证的几种方法的相对强度，包括在这个项目中开发的，使用一组新的可扩展的基准问题（自动驾驶汽车的导航问题，加压气体管道的泄漏检测算法等）。