MSc theses proposals

For more details about any of these proposals please contact its proponent:

(1) Enforcing model consistency with minimal repairs (Alcino Cunha)

Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models may coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Recently, we have developed the Echo framework (https://github.com/haslab/echo) to automatically enforce consistency between different models, based on the OMG bidirectional model transformation language QVT-R. Our framework is solver based (currently implemented on top of Alloy), and ensures that an update to one of the models is automatically propagated in a minimal way to the remaining ones in order to recover consistency. The main problem of this framework is efficiency: currently it only handles well models with sizes up to the hundreds of elements, which is far from the realistic model sizes required in industrial applications. The goal of this thesis is to pursue the developing of the Echo framework, and explore different techniques to increase its efficiency. Some of the techniques to consider include solver based approaches, such as MaxSat solvers (http://en.wikipedia.org/wiki/Maximum_satisfiability_problem), to speed up the generation of satisfying instances with minimal differences to a given target instance, or heurisitic techniques developed in the model repair research area, such as the one described in http://dl.acm.org/citation.cfm?id=2351707.

This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.

(2) A cookbook of bidirectional model transformations (Alcino Cunha)

Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models mays coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Bidirectional model transformation tools promise to ease this task, by enabling the user to write once and for all a specification that states how two models are to be kept consistent, and then automatically propagating updates in one model to updates in the other, in order to recover consistency according to that specification. There are many bidirectional transformation tools and languages, sometimes differing considerably in their features and expressiveness, making it difficult for a newcomer to access which is more adequate to his specific needs. The goal of this thesis is to develop a cookbook of paradigmatic bidirectional model transformation examples, deployed in different languages and tools. Besides helping software engineerings develop their own bidirectional model transformations, this cookbook will also act as a comparative survey of the existing tools and languages, helping pinpoint their similarities and idiosyncrasies in the context of concrete examples.

This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.

(3) Formal support for modeling and quantitative analysis of the reliability of safety critical systems (J.N. Oliveira)

Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. Extreme care is necessary given that a failure of the system may result in severe consequences. A rigorous analysis must consider the combination of the system behavior together with the domain assumptions and constraints of the environment where the system is to operate. Effective results should conduct to the identification of new (safety) requirements that help preventing the identified hazards and complement the initial system requirements. The purpose of this work is to develop a strong formally supported process for the modeling and quantitative analysis of high-assurance systems. The formal support should contribute both to the safety analysis process and to the subsequent derivation of safety requirements and/or system constraints. The work is to be based both on well-established analysis techniques such as fault propagation and novel paradigms that involve human-automation interactions and hazardous control actions.

The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.

This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.

(4) Techniques for automatic representation of requirements for critical software systems in multiple views. (Alcino Cunha)

Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. In this process, getting the requirements right is key: it is against them that the final system behavior is analyzed and verified. Errors introduced and not detected at the requirements stage propagate throughout the development and are later much more costly to correct. The purpose of this work is to assist engineers developing and validating systems’ and software requirements, combining multiple viewpoints to their definition and analysis. Each view represents a subset of the relevant attributes of the system. Complementary views include, for example, structural, functional, behavioral, and data flow. The goal is to develop a set of automatic bidirectional transformations between the different views in order to be able to generate, update, and keep consistent the information visible in each viewpoint.

The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.

This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.

(5) Calculating risk in component-oriented software systems using the LAoP (J.N. Oliveira)

Fault-injection exercises already undertaken in functional programs promise to scale up fault propagation calculation from stand-alone programs to architectures based on software-components. This will provide a semantically richer alternative to similar metrics produced elsewhere on the basis of call graphs and heuristic methods.

In this project we wish to experiment with injecting faults in coalgebric semantic models of component-based systems and derive algebraic laws enabling one to reason about how faults propagate in such systems and how they could be mitigated. From the same LAoP formalization one should obtain other quantitative (QoS) analyses of component systems just by changing the underlying (cost) semiring.

Experiments will be carried out a probabilistic extension to the monadic animation of the component algebra already used in the PAS module.

This proposal is supported by a grant of FCT project NASONI - Heterogeneous software coordination: Foundations, methods, tools(PTDC/EEI-CTP/2341/2012).

(6) Proposals by Altreonic (Altreonic/MFES team)

The following document contains directions for a partnership between MFES and this well-known innovative SME focusing on the embedded market. In particular, it contains themes for MSc theses to start in the following academic year: