A Unified Framework for Improving the Reliability of Reactive Systems

9619910诸如电信系统和飞机导航系统等被动系统与其环境不断相互作用，通常对安全至关重要。这就需要一个严谨的框架来论证它们的正确性。确保系统可靠性的传统形式化方法执行静态分析，其中使用定理证明和模型检查等技术验证高级设计。由于实际的系统比经过验证的抽象复杂得多，静态分析是通过测试和监视实现来补充的。该项目将引入严格的范式来监测反应系统，并将它们与静态分析技术一起使用，以获得系统行为正确性的数学保证。它的目标是扩展两个范例——程序检查，它试图通过检查证明结果是正确的来跟踪程序的每次计算，以及一致性测试，它试图通过观察其输入-输出行为来确定实现是否正确——到响应系统的上下文中。该项目还将探索分布式反应系统的分布式监控。＊＊＊

9619910 Reactive systems such as telecommunications systems, and aircraft navigation systems interact continuously with their environment and are usually safety critical. This has created a demand for a rigorous framework for reasoning about their correctness. Traditional formal methods for ensuring system reliability perform a static analysis where a high-level design is verified using techniques such as theorem proving and model checking. Since actual systems are much more complex than the verified abstraction, static analysis is supplemented by testing and monitoring of the implementation. This project will introduce rigorous paradigms for the monitoring of reactive systems and use them along with static analysis techniques to obtain mathematical guarantees on the correctness of system behaviors. It aims to extend two paradigms --- program checking, which seeks to follow up each computation of a program by a check that proves that the result is correct, and conformance testing, which seeks to determine if an implementation is correct by observing its input-output behavior --- to the context of reactive systems. The project will also explore distributed monitoring of distributed reactive systems. ***