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号州际公路旅行走廊的真实交通数据进行了测试。 该项目的教育组成部分包括有关交通网络建模和控制的课程开发，特别是该项目的正式方法方法，以及组织研讨会，以培训交通工程师和运营从业人员的使用软件工具和项目的方法。为了满足使用时间逻辑表达的丰富控制目标，该项目利用了现有，经过验证的流量模型的分段仿射性质，并得出有效的有限状态抽象，构成了正确构建控制综合的基础。 为了确保可伸缩性，该项目进一步利用了固有的单调性属性，并将其分解为稀疏连接的子系统。第一个研究任务是为信号时机和坡道计量策略开发一个设计框架，用于信号交叉点和高速公路交通控制。 第二个任务是对高速公路Onramps的协调控制和附近的信号交叉路口，以解决体育事件后的高速公路需求激增，或者在必须调整信号设置时在高速公路上发生事故以偏向于弯路。 第三个任务是进行设计，以利用对概率正确性保证的需求的统计数据以及包含最佳需求的设计，例如最大程度地减少旅行时间。 通过使用来自210号州际旅行走廊的流量数据校准的高保真仿真模型，对结果进行验证。