Abstract
Large distributed software systems are difficult to configure, maintain and operate. This complexity gives rise to frequent configuration errors [Oppenheimer03,Yin11]. One way to alleviate these errors is to develop methods to ensure the correctness of configurations during the system’s lifetime. Several static analysis methods have been proposed for verifying the correction of static configurations, including type systems, constraint satisfaction, model checking, … Verifying the correctness of configurations that may evolve over time has been far less studied. The goal of the thesis is to develop analysis tools for the verification of modular dynamic software systems, i.e. software systems made of potentially large collections of interacting components, whose structure and contents may evolve and be modified continuously. A first objective of the thesis is to formally characterize key software architecture properties, their forms of evolution, and the associated classes of errors that may occur at different times (e.g. assembly, deployment and operation). The main contributions of the thesis will consist in automated or semi-automated, static or dynamic, analysis techniques to detect and prevent the identified classes of errors. Inspiration can be taken from two related research domains:
-
ensuring static properties of systems like type systems characterizing interactions taking place in software architectures as in [Lienhardt08] or logical characterizations of graph properties as in [Geneves07];
-
ensuring the preservation of properties during dynamic evolutions as in works ensuring invariants on pointer data structures [Fradet97, Sagiv02] or in dynamic software architectures [LeMetayer98, Bruni08].
