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. ***