Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About
Download Photo HD

About

I am assistant professor at the Department of Informatics of Universidade do Minho, where I regularly teach courses on programming and formal methods for software engineering, and also a member of the High-Assurance Software Laboratory of INESC TEC. In recent years, my research is focused on the topic of formal methods for software engineering, namely developing new languages and tools for formal modeling, including validatiom and verificaiton, and for bidirectional model transformation. Recently, I've also started to research the topic of robotic software quality, in particular software developed for the Robot Operating System.

Interest
Topics
Details

Details

  • Name

    Alcino Cunha
  • Cluster

    Computer Science
  • Role

    Centre Coordinator
  • Since

    01st November 2011
005
Publications

2019

Static-Time Extraction and Analysis of the ROS Computation Graph

Authors
Santos, A; Cunha, A; Macedo, N;

Publication
Proceedings - 3rd IEEE International Conference on Robotic Computing, IRC 2019

Abstract
The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system's architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before. © 2019 IEEE.

2019

Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum

Authors
Cunha, A; Macedo, N;

Publication
International Journal on Software Tools for Technology Transfer

Abstract
This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification. © 2019, Springer-Verlag GmbH Germany, part of Springer Nature.

2019

Simplifying the Analysis of Software Design Variants with a Colorful Alloy

Authors
Liu, C; Macedo, N; Cunha, A;

Publication
Dependable Software Engineering. Theories, Tools, and Applications - 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019, Proceedings

Abstract
Formal modeling and automatic analysis are essential to achieve a trustworthy software design prior to its implementation. Alloy and its Analyzer are a popular language and tool for this task. Frequently, rather than a single software artifact, the goal is to develop a full software product line (SPL) with many variants supporting different features. Ideally, software design languages and tools should provide support for analyzing all such variants (e.g., by helping pinpoint combinations of features that could break a property), but that is not currently the case. Even when developing a single artifact, support for multi-variant analysis is desirable to explore design alternatives. Several techniques have been proposed to simplify the implementation of SPLs. One such technique is to use background colors to identify the fragments of code associated with each feature. In this paper we propose to use that same technique for formal design, showing how to add support for features and background colors to Alloy and its Analyzer, thus easing the analysis of software design variants. Some illustrative examples and evaluation results are presented, showing the benefits and efficiency of the implemented technique. © Springer Nature Switzerland AG 2019.

2019

Simulation under Arbitrary Temporal Logic Constraints

Authors
Brunel, J; Chemouil, D; Cunha, A; Macedo, N;

Publication
Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019.

Abstract
Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode cannot take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework. © J. Brunel, D. Chemouil, A. Cunha, & N. Macedo.

2018

Proposition of an Action Layer for Electrum

Authors
Brunel, J; Chemouil, D; Cunha, A; Hujsa, T; Macedo, N; Tawa, J;

Publication
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings

Abstract

Supervised
thesis

2016

Parallel verification of Dynamic Systems with Rich Configurations

Author
Eduardo Jose Dias Pessoa

Institution
UM

2016

0

Author
Rosária Maria Afonso Rodrigues de Melo

Institution
UP-FCNA

2016

Safety Verification for ROS Applications

Author
André Filipe Faria dos Santos

Institution
UM

2016

-

Author
Chong liu

Institution
UM

2016

A Web-based Social Environment for Alloy

Author
José Manuel Costa Pereira

Institution
UM