Titulo Estágio
Automating Formal Analysis of Self-Adaptation in Rainbow
Áreas de especialidade
Engenharia de Software
Local do Estágio
CISUC/SSE
Enquadramento
Modern software systems are increasingly pervasive, and tend to operate in unpredictable environments. Self-adaptive systems are able, not only to recover from system failures, but also to deal with more subtle conditions (degradation in performance, …). In particular, there has been substantial research in the use of architectural models that provide a high-level view of the system, enabling flexible adaptation when dealing with complex situations.
Unfortunately, flexibility comes at the price of reducing the predictability of adaptation mechanisms with respect to the limits of the system while undergoing adaptation. How can one assess if a particular alternative for adaptation is better than another one, or that a particular repair will not make the situation worse?
One of the alternatives to answer those questions is making use of formal analysis techniques (e.g., probabilistic model checking) to model and predict the behavior of the system under different adaptation alternatives.
Objetivo
The goal of this work is to gather the requirements and implement a translator between Stitch (a language for specifying adaptation strategies in Rainbow, a framework used to build architecture-based self-adaptive systems developed at CMU), and PRISM (a probabilistic model checking tool that enables formal analysis of stochastic systems).
Specifically, the translator must be able to use as input a Stitch adaptation model, which comprises a set of adaptation tactic (primitive adaptation actions) and strategy specifications, and produce a valid PRISM model suitable for model checking of properties. The translation scheme will be based upon an existing specification of Stitch adaptation model encodings in PRISM. Finally, the translator must be extensible and able to integrate Stitch language extensions that can be developed in the future.
Plano de Trabalhos - Semestre 1
This work includes the following activities:
(a) [2014-09-01 to 2014-10-31] The review of the state-of-the-art;
(b) [2014-11-01 to 2015-01-31] Requirements analysis and architecture definition;
(c) [2014-12-01 to 2015-01-31] Write Thesis Proposal
Plano de Trabalhos - Semestre 2
(d) [2015-02-01 to 2015-04-30] Specification and implementation of a reference infrastructure for prototype evaluation;
(e) [2014-11-01 to 2014-04-30] Prototype implementation and evaluation;
(f) [2015-04-01 to 2015-05-31] Write a paper;
(g) [2015-03-01 to 2015-07-31] Write the thesis;
Condições
The work is to be executed at the laboratories of the CISUC’s Software and Systems Engineering Group. A work place will be provided as well as the required computational resources.
Observações
This internship will be in collaboration with Carnegie Mellon University (CMU).
CMU Co-advisers:
- Javier Camara Moreno (jcmoreno@cs.cmu.edu) and Bradley Schmerl (schmerl+@cs.cmu.edu) and
DEI Co-advisers:
- Jorge Bernardino (jorge@isec.pt) and Pedro Furtado (pnf@dei.uc.pt)
(inserido pelo coordenador do MEI)
Informação sobre se o estágio é ou não remunerado não foi inserida pelos proponentes.
Orientador
Javier Camara Moreno and Jorge Bernardino
jorge@isec.pt 📩