ARCA

Software Architectures & Design Calculi

Research team @ HASLab, Univ. Minho

Arca Foundations

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.

Arca is grounded on 3 fundamental pilars:

Software Components
Lead by Renato Neves, Arca investigates component models and calculi that abstract different computational paradigms. These abstractions include partiality, non-determinism, fuzziness, probabilistic evolution, continuity, quantum, and biology.
Software Architectures
Lead by José Proença, Arca analyses and formalises how heterogeneous and concurrent components interact, inspired by the Reo coordination language. The investigated models and calculi for coordination address notions such as variability and reconfigurability.
Logics
Lead by Alexandre Madeira, Arca studies how to use logics, in particular modal logics, to specify and verify properties of computational systems, both at the component and the architecture level. This study is generic and later adapted to specific paradigms and application areas.

Tweets

Members

Research Associates

Former members

Key Publications since 2015

Tools

Check our GitHub site at https://github.com/arcalab.

Contributions

List of contributions to other projects.
  • Hets - Added support for HybridCASL, providing a method to automatically combine the standard properties of hybrid logics with any logic already integrated in Hets.

Projects

Collaboration

We are also involved in the following projects.
  • LightKone

    LightKone

    Lightweight computation for networks at the edge; 2017–2020.

  • TRUST

    TRUST

    Trustworthy Software Design with Alloy; 2016–2018.

  • SmartEGOV

    (P2020 NORTE-45-2015-23) Harnessing EGOV for smart governance: Foundations and tools, since May, 2016.

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.

Past Projects

Projects
  • NASONI: Heterogeneous software coordination: Foundations, methods, tools; 2013-2015.
Dissertations
  • [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.

Courses

  • Mathematics for Computer Science (2017/18) An introductory course to Logic and Relations given to external students.
  • Software architecture and Calculi (2015/16, 2016/17) For Master students, on how to model and analyse concurrent systems.
  • Interaction and Concurrency (2016/17) 3rd year course on process algebra and other concurrency models.
  • Algebraic and Coalgebraic Models in Software Development (2016/17) For PhD students - Doctoral program of MAP-i, including the universities of Minho, Aveiro and Porto.
  • Quantum Logic (2017/18)
  • Quantum Computing (2016/17)

Research Opportunities

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

(Funded by either the Trust or the DaLí project.)

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

(Funded by the Trust project.)

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

(Funded by the DaLí project.)

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

(Funded by either the Trust or the DaLí project.)

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

(Funded by the DaLí project.)

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.

Dissemination events

Arca Meetings

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

Upcoming meetings

Previous meetings