Scalable algorithms for safety verification and reachability analysis of hybrid systems

用于混合系统安全验证和可达性分析的可扩展算法

• 批准号: 0611925
• 负责人: Calin Belta
• 金额: $ 20.8万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-07-01 至 2008-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0611925&HistoricalAwards=false
• 关键词: Scalable; algorithms; safety; verification; reachability

In the past few decades, there have been tremendous advances in microprocessor technology and the use of digital controllers in the automation of physical plants. The increasing integration of such controllers results in highly complex systems involving both continuous and discrete event dynamics. In addition to discontinuities introduced by the computer, most physical processes exhibit discrete dynamics due to the action of elements ranging from valves, gears and switches in electromechanical systems to transcriptional regulators in genetic and metabolic networks. Such systems combining discrete and continuous features are called hybrid systems.Formal verification is a very important issue during system design. Its goal is to prove that the system performs as expected. As the automated systems are growing in scale and complexity, the possibility of subtle errors is much greater. This project develops scalable, provably correct algorithms and software tools for safety verification and reachability analysis of hybrid systems. First, the project investigates the construction of discrete abstractions. While doing this, this work attempts to enlarge the class of known decidable hybrid systems. Second, enabled by recent advances in semialgebraic methods and convex optimization, the project investigates a new method for safety verification that does not require explicit calculation of trajectories or reachable sets, and provides a nested family of sufficient conditions for system safety that are polynomial-time checkable. Third, bringing ideas from motion planning based on randomized techniques, the project develops an algorithm for test case generation.The algorithms developed in this project are implemented as a Reachability Analysis and VErification (Rave) toolkit and tested by considering two very difficult problems arising in the safety of multi-agent robotic systems. The results of this project also have an immediate impact in a wide range of areas where hybrid systems are used for modeling, such as automated highway systems, air-traffic management systems, genetic and metabolic networks, embedded automotive and avionic controllers, robotics, and real-time communication networks.

在过去的几十年里，微处理器技术和数字控制器在物理工厂自动化中的应用取得了巨大的进步。这种控制器的集成度越来越高，导致了涉及连续和离散事件动力学的高度复杂系统。除了计算机引入的不连续性外，大多数物理过程由于从机电系统中的阀门、齿轮和开关到遗传和代谢网络中的转录调节因子等元素的作用而表现出离散动力学。这种结合了离散和连续特征的系统称为混合系统。形式化验证是系统设计中一个非常重要的问题。它的目标是证明系统按预期运行。随着自动化系统在规模和复杂性上的增长，发生细微错误的可能性要大得多。该项目开发可扩展的、可证明正确的算法和软件工具，用于混合系统的安全验证和可达性分析。首先，该项目研究了离散抽象的构造。在这样做的同时，这项工作试图扩大已知的可决定混合系统的类别。其次，由于半代数方法和凸优化的最新进展，该项目研究了一种新的安全验证方法，该方法不需要显式计算轨迹或可达集，并为系统安全提供了一套多项式时间可检查的充分条件。第三，引入基于随机化技术的运动规划思想，该项目开发了一种用于生成测试用例的算法。本项目开发的算法作为可达性分析和验证（Rave）工具包实现，并通过考虑多智能体机器人系统安全性中出现的两个非常困难的问题进行测试。该项目的成果也对混合系统用于建模的广泛领域产生了直接影响，例如自动高速公路系统、空中交通管理系统、遗传和代谢网络、嵌入式汽车和航空电子控制器、机器人和实时通信网络。