Combining Monitors through Assume Guarantee Reasoning

From Anita Borg Institute Wiki

Presenter: Haiqiong Yao (University of South Florida)

Runtime monitoring provides the confidence of the implementation of the system. It prefers to check simple properties since the process of verification consumes the resources limited in a machine. But monitoring multiple properties in a single large monitor is error-prone. Cooperation of several smaller monitors instead of a single one is reasonable. We propose an approach to applying assume-guarantee reasoning in combining monitors to guarantee the soundness of runtime monitoring.