Research Report A55: A Rule-Based Formal Method for Software Configuration

Author: Tommi Syrjänen

Date: Dec 1999

Pages: 74

In this work we examine the software configuration management problem. We give a short introduction to the current state of the art and present a declarative rule-based formal language for representation of configuration knowledge. As a novel feature, the rule language allows finite existential quantification over the configuration components. We show a translation from the rule language to normal logic programs with stable model semantics. As a case study we examine the configuration management problem for the Debian GNU/Linux system which consists of over 2000 distinct software packages. We examine the current practice to identify the main components of the problem and present a way to formalize them using the rule language. We construct two formal models: one for finding valid configurations and one for diagnosing unsatisfiable user requirements. We show that the decision problem for the configuration model is NP-complete. We present a translator that reads a high-level description of the Debian configuration system and produces the corresponding set of rules. We evaluate the configuration model by using actual data from Debian version 2.1 and a set of randomly generated user requirements. The evaluation shows that the model is computationally feasible.

Keywords: Configuration management, stable model semantics, logic programming, Debian, Linux, diagnostics


Full report in Postscript