Sound Programming of Adaptive Dependable Embedded Systems
HomeAnalysis and types for safe dynamic software configurations
Analysis and types for safe dynamic software configurations
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].
Analysis techniques that can be considered include type checking, compatibility checking (as in session types [Gay10]), as well as constraint satisfaction and model checking. It is expected that the analysis techniques developed as part of the thesis will be prototyped and their usefulness evaluated by application in particular to cloud application deployment.
The thesis will take place in the INRIA SPADES team, in Grenoble, France. The SPADES team conducts research on programming dependable embedded systems. As part of that effort, the team develops new formal component models, programming languages and associated tools for verification, analysis or synthesis.
Candidates for this thesis should have a strong background on formal methods. Good knowledge of type systems, static analysis and/or model checking are a plus. Good programming skills for the prototype development envisaged, and an appetite for useful tools grounded on sound theory, would be appreciated as well.