Analysis and types for safe dynamic software configurations

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].
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.
Context
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.
Expertise required
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.
Candidates are invited to send their application to Jean-Bernard Stefani (jean-bernard.stefani@inria.fr) and Pascal Fradet (pascal.fradet@inria.fr). Please include at least a CV, a short motivation letter and contact information for 2 referees.
References
[Bruni08] R. Bruni, A. Lluch-Lafuente, U. Montanari: Style-Based Architectural Reconfigurations. Bulletin of the EATCS 94: 161-180 (2008)
[Fradet97] P. Fradet, D. Le Métayer: Shape Types. POPL 1997: 27-39
[LeMetayer98] D. Le Métayer: Describing Software Architecture Styles Using Graph Grammars. IEEE Trans. Software Eng. 24(7): 521-533 (1998)
[Lienhardt08] M. Lienhardt, A. Schmitt, J.B. Stefani: Typing communicating component assemblages. GPCE 2008.
[Gay10] S. J. Gay, V. T. Vasconcelos, A. Ravara, N. Gesbert, A. Z. Caldeira: Modular session types for distributed object-oriented programming. POPL 2010.
[Geneves07] P. Genevès, N. Layaïda, A. Schmitt: Efficient static analysis of XML paths and types. In PLDI 2007.
[Oppenheimer03] D. L. Oppenheimer, A. Ganapathi, D. A. Patterson: Why Do Internet Services Fail, and What Can Be Done About It? USENIX Symposium on Internet Technologies and Systems 2003.
[Sagiv02] S. Sagiv, T. Reps, R. Wilhelm: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3): 217-298 (2002) [Stefani14] J.B. Stefani: Components as Location Graphs. FACS 2014.
[Yin11] Z. Yin, X. Ma, J. Zheng, Y. Zhou, L. N. Bairavasundaram, S. Pasupathy: An empirical study on configuration errors in commercial and open source systems. SOSP 2011.