Software Architectures & Design Calculi

Research team @ HASLab, Univ. Minho

About Arca

Arca – Software Architecture & Design Calculi – is a research team lead by prof. Luís Barbosa and prof. José Nuno Oliveira. It investigates formal approaches based on calculi of programs, processes, algorithms, etc. and on software quality, focusing on components, architectures, coordination, and variability.

This team is part of the HASLab group, which is a software laboratory the university of Minho associated to INESC TEC.



Existing Projects

  • DaLí: Dynamic logics for cyber-physical systems; 2016–2018.
  • TRUST: Trustworthy Software Design with Alloy; 2016–2018.
  • NASONI: Heterogeneous software coordination: Foundations, methods, tools; 2013-2015.

Ongoing PhD and Master projects

  • [PhD] Logics and calculi for cyber–physical components, by Renato Neves.

    Supervisor: Luís Barbosa.

    This project focuses mainly on the foundations of cyber physical systems; coalgebras, proof theory and institutional theory. It also covers a myriad of logics, in particular modal logics.

  • [PhD] A Virtual Factory for Smart City Service Integration, by Guillermina Cledou.

    Supervisors: Luís Barbosa and Elsa Estevez.

    The aim of the thesis is to advance the state of the art in software modelling and development tools for the rapid development of integrated city-level electronic public services.

  • [PhD] Quantum algebraic specifications, by Carlos Tavares.

    Supervisor: Luís Barbosa.

    This project investigates algebraic approaches to specify and analyse quantum computer science.

  • [PhD] Dynamising dynamic logic, by Leandro Gomes.

    Supervisor: Luís Barbosa.

    This project aims at building a systematic process of generating dynamic logic, by developing a general theory of such logics. This approach favours a contract-based design method for software specification, and the development of an algebraic structure to model the space of programs and the corresponding domains of behaviours.

  • [Master] Animation of monad H, by Tiago Loureiro.

    Supervisors: Luís Barbosa and Renato Neves.

    This project proposes an Haskell implementation for hybrid systems, capable of visually depicting the evolution of continuous functions.

Open topics

These is a selection of possible projects for master students that would like to work with us. We are also open for discussion about other topics. Note that we have a few grants that can pay for most of the ideas presented in these projects. If you are interested, just come and talk to us.

Alloy and Hybrid Logic

The purpose of this project is to explore a variant of hybrid logics in which worlds are equipped with Alloy models. In principle, such a logic (generated via the hybridisation method "hybridisation") provides a canonical language to address reconfigurability in Alloy specifications.

The workplan involves the implementation of a calculus for this logic (reported in Proof theory for hybridised logics) and the development of a case study that illustrates its potentialities (and limitations) in the software development process.

Model checking R/G programs in Alloy

When you run a program on your lap-top you "rely" on the operating system not letting any other program to interfere with your state space. But programs could be designed in a collaborative-style, with sub-programs helping each other over a shared state. (Example: on-the-fly garbage collection.) In the early 1980s, Cliff Jones proposed a dynamic extension to (static) Hoare logic: further to pre / post conditions, one could also specify interference of the environment via rely / guarantee conditions. Interest on R/G programming is growing a lot due to its potential for concurrency.

In this project we would like to use Alloy to model the semantics of a simple imperative language with R/G commands and model-check their interference. The idea is to find design errors of (possibly non-terminating) R/G programs by analysing finite traces only.

From specifications to concrete processes

This project aims at studying a dynamic logic with binders, and (automatic) translations from specifications in (some fragment) of this logic into a concrete process algebra.

Reo families in your browser

This project aims at producing an extensible web-based framework to specify and analyse systems of coordinated components. It will involve developing a web-oriented framework for Reo connectors, possibly with a graphical frontend, and designing an extensible architecture with clear separations between the core model, the frontends, and the backends. To illustrate the extensibility of the framework, an extension for parameterised Reo connectors should be developed.

Quantum Programming Languages

This project aims at exploring the field of quantum programming languages and quantum artificial intelligence in a new line of research of the group of formal methods of Department of Informatics. The project involves the implementation of some quantum algorithms and its comparison with more classical approaches.

[PhD] Making Logics Coalgebraic

The main goal of this PhD project is the development of a general notion of asymmetric combination of logic that turns logics coalgebraic. More concretely, a process that equips any given logic with suitable coalgebraic machinery re- spective to a given functor; this means that, in contrast to hybridisation, or temporalisation, the input parameter is not just the base logic, but also the functor that gives rise to the intended type of transitions.

Arca Meetings

We meet every two weeks to discuss ongoing work within the team.

Upcoming meetings

Previous meetings