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