Available Theses on the Topic of Building Autonomic Systems through SelfLets

Verification of Highly Distributed Autonomic Systems in a rely-guarantee fashion

Highly-distributed systems are typically large systems composed of many elements interacting with one another. When dependability for these systems is a concern, being able to model and analyze their properties, especially non-functional ones, in a formal and automated way becomes essential. This is particularly important when systems must be autonomic. That is, when they need to be able to self-manage to adjust to the situation of the environment. Often, however, the application of formal methods and automated reasoning is seen by practitioners as complex and time consuming. Compositional techniques can help modify this belief. In [1] we present a compositional technique and show that it can suitable for the description and verification of a specific distributed and autonomic system.

• the application of our approach to other case studies, possibly more complex than the one we have considered so far;
• the identification of compositional patterns that can be exploited in the formalization and analysis of more than one system
• the refinement of the approach for what concerns the modeling of the autonomic characteristics of system components and of the mechanisms through which they communicate.

Integration of different paradigms in the analysis of dependability properties of autonomic systems

Analyzing dependability properties of autonomic systems is a challenging proposition, since these systems are intrinsically built to evolve during their execution. As such, they cannot be analyzed at design time against all possible situations and configurations in which they operate. They can, however, be analyzed under different conditions, which may have different probability to occur. Analysis subject to external conditions is a staple of rely-guarantee approaches, in which the properties of a module are checked under suitable assumptions on the environment with which it interacts. Combining such approaches with probabilistic analysis would allow us to get a fuller and more complete picture of the properties of dynamic systems under changing assumptions.

We are currently developing rely-guarantee and probabilistic analysis techniques in different projects. The goal of this thesis is to study how to combine them in a single technique that we will validate on some significant case study. Interested readers can refer to the following bibliography for more details about autonomic systems and the techniques we plan to exploit:

Formal modeling of autonomic systems

Autonomic services are suitable building blocks for highly dynamic applications that must adapt to changing environments, contexts, requirements. When these applications combine a high level of dynamism with dependability requirements (e.g., health care systems), the components on which they are built must be precisely designed and their properties must be well understood. Modeling these components in a formal way can help in this regard.

The goal of this thesis is to further develop an existing formal model of the concept of SelfLet, the building block of an autonomic infrastructure that is being developed in our research group. The existing formal model includes the core elements of the SelfLet component; however, it still lacks a number of concepts, and especially those related to the autonomic mechanisms on which the SelfLet infrastructure is based. The goal of the model is to build a "theory of SelfLets" (for example through the demonstration of relevant properties of the SelfLet infrastructure), on which sound, dependable autonomic systems can be built.

Contacts: