paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fault-tolerant functional reactive programming (extended version)

容错函数式反应式编程(扩展版)
JFP vol.302020匹配度 2/10 · 该论文属于函数式反应式编程与类型系统中的容错/形式化保障,和静态分析、形式化验证有很弱的领域关联,但不涉及 LLM/Agent、ML 系统分析、浮点程序分析或贝叶斯程序分析,未命中用户的核心追题。引用 4 inbox
IVAN PEREZ, ALWYN E. GOODLOE
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:将容错机制引入函数式反应式编程,在值层注入故障并在类型层保证容错性质。

医学、航空航天等关键领域需要严格设计与验证,函数式语言已被用于构建反应式系统的同步数据流语言,函数式反应式编程(FRP)以优雅且鲁棒的方式刻画了其核心。然而,现有 FRP 抽象虽常支持失败或终止,处理未知类型故障并将容错机制集成进 FRP 仍是开放问题。本文扩展已有 FRP 框架以支持容错:在值层,为故障信号标注可靠性与概率信息,并通过随机测试注入故障、用时序逻辑验证系统性质;在类型层,用组件可能表现出的故障种类进行标注,并借助类型级编程获得容错关键方面的编译期保证。作者表明该方法足以应对现实复杂度系统,并能灵活用于系统分析与设计、故障存在下的性质验证、运行时监控以及不同容错机制效果研究。

问题
关键反应式系统需在高负载下长期运行,但现有 FRP 抽象对未知类型故障及容错机制的集成支持不足。
方法
扩展现有 FRP 框架:值层用可靠性与概率标注故障信号并随机注入故障、以时序逻辑验证性质;类型层用故障种类标注组件并通过类型级编程提供编译期容错保证。
评估
作者从现实复杂度适用性与灵活性两方面论证方法,展示其可用于系统分析设计、故障下性质验证、运行时监控和比较不同容错机制。
原文摘要(Abstract)

Abstract Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation, and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and functional reactive programming (FRP) capture the essence of those languages in a way that is both elegant and robust. To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many functional reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults , and incorporating fault tolerance into FRP, requires a different construction and remains an open problem. This work demonstrates how to extend an existing functional reactive framework with fault tolerance features. At value level, we tag faulty signals with reliability and probability information and use random testing to inject faults and validate system properties encoded in temporal logic. At type level, we tag components with the kinds of faults they may exhibit and use type-level programming to obtain compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide system analysis and design, validate system properties in the presence of faults, perform runtime monitoring, and study the effects of different fault tolerance mechanisms.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{PerezG20,
  title = {Fault-tolerant functional reactive programming (extended version)},
  author = {IVAN PEREZ and ALWYN E. GOODLOE},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796820000118}
}