CPS: Synergy: Collaborative Research: Efficient Traffic Management: A Formal Methods Approach

CPS：协同：协作研究：高效交通管理：形式化方法

• 批准号: 1446151
• 负责人: Calin Belta
• 金额: $ 30.15万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1446151&HistoricalAwards=false
• 关键词: CPS; Synergy; Collaborative; Research; Efficient

Title: Efficient Traffic Management: A Formal Methods ApproachThe objective of this project is to develop a formal methods approach to traffic management. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction. This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc. The task is then to design signal timing and ramp metering strategies to meet such specifications. To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques. The results are tested with real traffic data from the Interstate 210 travel corridor in Southern California. The educational component of the project includes course development on modeling and control of traffic networks, featuring in particular the formal methods approach of this project, and organizing workshops to train traffic engineers and operation practitioners on the use of software tools and methodologies of the project. To meet rich control objectives expressed using temporal logic, the project exploits the piecewise affine nature of existing, validated traffic models, and derives efficient finite state abstractions that form the basis of correct-by-construction control synthesis. To ensure scalability, the project further takes advantage of inherent monotonicity properties and decomposibility into sparsely connected subsystems. The first research task is to develop a design framework for signal timing and ramp metering strategies for signalized intersections and freeway traffic control. The second task is the coordinated control of freeway onramps and nearby signalized intersections to address situations such as a freeway demand surge after a sporting event, or an accident on the freeway when signal settings must be adjusted to favor a detour route. The third task is to pursue designs that exploit the statistics of demand for probabilistic correctness guarantees, as well as designs that incorporate optimality requirements, such as minimizing travel time. Validation of the results is pursued with high-fidelity simulation models calibrated using traffic data from the Interstate 210 travel corridor.

标题：高效交通管理：一种正式的方法方法本项目的目标是开发一种正式的方法方法来进行交通管理。形式化方法是计算机科学的一个领域，它开发有效的技术来证明系统的正确操作，例如计算机程序和数字电路，并用于设计通过构造而正确的系统。该项目将这种形式主义扩展到交通网络，其中的正确性规范包括消除拥堵、确保高速公路吞吐量保持在最小阈值以上、队列始终最终被清空等。然后任务是设计信号配时和匝道计量策略以满足这些规范。为了完成这项任务，该项目利用了现有的、经过验证的交通流数学模型的内在结构，并开发了计算高效的设计技术。结果用南加州210号州际公路出行走廊的真实交通数据进行了测试。该项目的教育部分包括开发关于交通网络建模和控制的课程，特别介绍该项目的正式方法方法，并组织讲习班，培训交通工程师和操作从业人员使用该项目的软件工具和方法。为了满足用时态逻辑表达的丰富的控制目标，该项目利用了现有的经过验证的流量模型的分段仿射性质，并推导出有效的有限状态抽象，形成了逐结构更正控制综合的基础。为了确保可伸缩性，该项目进一步利用了固有的单调性属性和可分解为稀疏连接的子系统。第一个研究任务是开发一个用于信号交叉口和高速公路交通控制的信号配时和匝道控制策略的设计框架。第二项任务是协调控制高速公路入口匝道和附近的信号交叉口，以应对诸如体育赛事后高速公路需求激增或高速公路上的事故等情况，此时必须调整信号设置以有利于绕行路线。第三项任务是寻求利用概率正确性保证需求统计数据的设计，以及包含最优要求的设计，如最小化行程时间。使用210号州际公路出行走廊的交通数据校准的高保真模拟模型对结果进行了验证。