CPS: TTP Option: Small: Consistency vs. Availability in Cyber-Physical Systems

CPS：TTP 选项：小：网络物理系统中的一致性与可用性

• 批准号: 2233769
• 负责人: Edward Lee
• 金额: $ 50万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-01-15 至 2025-12-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2233769&HistoricalAwards=false
• 关键词: CPS; TTP; Option; Small; Consistency

Distributed cyber-physical systems (CPS), where multiple computer programs distributed across a network interact with each other and with physical processes, are challenging to design and verify. Such systems are found in industrial automation, transportation systems, energy distribution systems, and many other applications. This project is developing a “systems theory” for such applications that provides a good analytical toolkit for understanding how a system will behave when networks misbehave. It is building tools that make it possible to reason about the design of safe and reliable distributed CPS applications in an accessible user-friendly environment. In distributed applications, Brewer's CAP theorem tells us that when networks become partitioned, there is a tradeoff between consistency and availability in distributed software systems. Consistency is agreement on the values of shared variables; availability is the ability to respond to reads and writes of those shared variables. This project builds on an extension that has shown that consistency, availability, and network latency can be quantified, and that the CAP theorem can be generalized to give an algebraic relation between these quantities. This generalization is called the CAL theorem because it replaces “network Partitioning” with “Latency,” where partitioning is just a limiting case of latency. The CAL theorem can be used to help design distributed systems that fail gracefully when network performance degrades. With increasing latency, either consistency or availability (or some measure of both) must be sacrificed, and the CAL theorem quantifies these sacrifices. This project is applying the CAL theorem to distributed CPS. The project is deriving the fundamental limits implied by the CAL theorem and developing a methodology for systematically trading off availability and consistency in application-specific ways. The application of the CAL theorem to CPS generalizes consistency to include agreement on the state of the physical world and availability to include the latency of software responses to stimulus from the physical world. Instead of focusing solely on network latency, the project adopts a measure called “apparent latency” that includes network latency plus all other sources of latency (e.g., computation time). This measure is practically measurable. The project builds upon the recently developed Lingua Franca coordination language to provide system designers with concrete analysis and design tools to make the required tradeoffs in deployable software. The tools automatically produce graphical renditions of systems and user-friendly feedback on the concurrent, distributed, and real-time aspects.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

分布式网络物理系统（CPS）是分布在网络上的多个计算机程序相互交互并与物理过程交互的系统，在设计和验证方面具有挑战性。这样的系统可以在工业自动化、运输系统、能源分配系统和许多其他应用中找到。这个项目正在为这样的应用程序开发一个“系统理论”，它提供了一个很好的分析工具包，用于理解当网络行为不正常时系统将如何表现。它正在构建工具，使在可访问的用户友好的环境中推理安全可靠的分布式CPS应用程序的设计成为可能。在分布式应用程序中，Brewer的CAP定理告诉我们，当网络被分区时，在分布式软件系统中存在一致性和可用性之间的权衡。一致性是对共享变量值的一致；可用性是对这些共享变量的读和写进行响应的能力。这个项目建立在一个扩展的基础上，这个扩展表明一致性、可用性和网络延迟可以被量化，并且CAP定理可以被推广到给出这些量之间的代数关系。这种概括被称为CAL定理，因为它用“延迟”取代了“网络分区”，其中分区只是延迟的一种极限情况。CAL定理可用于帮助设计分布式系统，使其在网络性能下降时优雅地失败。随着延迟的增加，必须牺牲一致性或可用性（或两者的某种度量），而CAL定理量化了这些牺牲。本项目将CAL定理应用于分布式CPS。该项目正在推导CAL定理所隐含的基本限制，并开发一种方法，以特定于应用程序的方式系统地权衡可用性和一致性。CAL定理在CPS中的应用将一致性推广到包括对物理世界状态的一致性，将可用性推广到包括软件对来自物理世界的刺激的响应的延迟。该项目没有仅仅关注网络延迟，而是采用了一种称为“表观延迟”的度量，它包括网络延迟加上所有其他延迟来源（例如，计算时间）。这一措施实际上是可以衡量的。该项目以最近开发的Lingua Franca协调语言为基础，为系统设计人员提供具体的分析和设计工具，以便在可部署软件中进行所需的权衡。这些工具自动生成系统的图形化再现，以及对并发、分布式和实时方面的用户友好反馈。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Consistency vs. Availability in Distributed Cyber-Physical Systems

分布式信息物理系统中的一致性与可用性

• DOI: 10.1145/3609119
• 发表时间: 2023
• 期刊: ACM Transactions on Embedded Computing Systems
• 影响因子: 2
• 作者: Lee, Edward A.;Akella, Ravi;Bateni, Soroush;Lin, Shaokai;Lohstroh, Marten;Menard, Christian
• 通讯作者: Menard, Christian

High-performance Deterministic Concurrency Using Lingua Franca

• DOI: 10.1145/3617687
• 发表时间: 2023-01
• 期刊: ACM Transactions on Architecture and Code Optimization
• 影响因子: 1.6
• 作者: Christian Menard;Soroush Bateni;Peter Donovan;Clément Fournier;Shaokai Lin;Felix Suchert;Tassilo Tanneberger;Hokeun Kim;J. Castrillón;Edward A. Lee

Towards Building Verifiable CPS using Lingua Franca

• DOI: 10.1145/3609134
• 发表时间: 2023-09
• 期刊: ACM Transactions on Embedded Computing Systems
• 影响因子: 2
• 作者: Shaokai Lin;Yatin A. Manerkar;Marten Lohstroh;Elizabeth Polgreen;Sheng-Jung Yu;Chadlia Jerad;Edward A. Lee;S. Seshia

Trading Off Consistency and Availability in Tiered Heterogeneous Distributed Systems

分层异构分布式系统中的一致性和可用性的权衡

• DOI: 10.34133/icomputing.0013
• 发表时间: 2023
• 期刊: Intelligent Computing
• 作者: Lee, Edward A.;Bateni, Soroush;Lin, Shaokai;Lohstroh, Marten;Menard, Christian
• 通讯作者: Menard, Christian