On observed reproducibility in network configuration management

A rigorous language for discussing the issue of configuration management is currently lacking. To this end, we develop a simple state machine model of configuration management. Observed behaviors comprise the state of a host and configuration processes accomplish state transitions. Using this language, we show that for one host in isolation and for some configuration processes, reproducibility of observed effect for a configuration process is a statically verifiable property of the process. Using configuration processes verified in this manner, we can efficiently identify latent preconditions that affect behavior among a population of hosts. Constructing configuration management tools with statically verifiable observed behaviors thus reduces the lifecycle cost of configuration management.