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