Configuration Monitor Synthesis

TL;DR

The paper tackles the problem of determining runtime configurations of configurable systems solely from observed behavior, even under imperfect observations. It introduces verdict transition systems ($VTS$) as a general, modular foundation that unifies automata-based runtime monitoring and fault diagnosis, and shows how to synthesize $VTS$s from featured transition systems ($FTS$) via an annotation-tracking pipeline. The approach supports partial observability, bounded delays and losses, and predictive (lookahead) verdicts, while guaranteeing soundness and completeness of configuration monitors and enabling determinization/minimization for efficient implementations. Empirical evaluation on configurable-systems benchmarks demonstrates scalable synthesis, significant size reductions through minimization, and meaningful diagnosis/monitoring capabilities, providing a unified explanation for family-based verification results. Overall, the framework offers a versatile, principled method to synthesize robust, predictive monitors and diagnosers across monitoring and diagnosis tasks.

Abstract

The observable behavior of a system usually carries useful information about its internal state, properties, and potential future behaviors. In this paper, we introduce configuration monitoring to determine an unknown configuration of a running system based on observations of its behavior. We develop a modular and generic pipeline to synthesize automata-theoretic configuration monitors from a featured transition system model of the configurable system to be monitored. The pipeline further allows synthesis under partial observability and network-induced losses as well as predictive configuration monitors taking the potential future behavior of a system into account. Beyond the novel application of configuration monitoring, we show that our approach also generalizes and unifies existing work on runtime monitoring and fault diagnosis, which aim at detecting the satisfaction or violation of properties and the occurrence of faults, respectively. We empirically demonstrate the efficacy of our approach with a case study on configuration monitors synthesized from configurable systems community benchmarks.

Figures (3)

• Figure 1: Model of an email system with an encryption ($\mathsf{e}$) and signing ($\mathsf{s}$) feature.
• Figure 2: Configuration verdict domain for the email system (\ref{['fig:email-model']}).
• Figure 3: Illustrative transition system model of a coffee machine.

Theorems & Definitions (6)

• definition thmcounterdefinition
• lemma thmcounterlemma
• proof
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition