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

About

I am currently a postdoc affiliated with HASLabUniversity of Minho, working with Luís Barbosa. Until January 2016 I was also affiliated with DistrinetKU Leuven, working mainly with Danny Hughes and Dave Clarke. My work is mainly on coordination of distributed components, often associated to the Reo coordination language, and on formal approaches to software product line engineering. More recently I have been working with binding and component models for embedded devices in the context of the LooCI middleware and micro PnP.

I graduated in University of Minho, Portugal, for a 5 year degree in Mathematics and Computer Science. I studied abroad for 6 months as an Erasmus student in Bristol University, UK. I defended my PhD in Leiden University in May 2011, for my work carried in CWI, Amsterdam, in the group for Foundations of Software Engineering.

Interest
Topics
Details

Details

  • Name

    José Paiva Proença
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st March 2013
001
Publications

2017

A Refinement Relation for Families of Timed Automata

Authors
Cledou, G; Proença, J; Barbosa, LS;

Publication
Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings

Abstract
Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional. © Springer International Publishing AG 2017.

2017

Composing Families of Timed Automata

Authors
Cledou, G; Proença, J; Barbosa, LS;

Publication
Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers

Abstract
Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain. © 2017, IFIP International Federation for Information Processing.

2017

Formal Verification of ROS-Based Robotic Applications Using Timed-Automata

Authors
Halder, R; Proenca, J; Macedo, N; Santos, A;

Publication
5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2017, Buenos Aires, Argentina, May 27, 2017

Abstract

2017

Quality-Aware Reactive Programming for the Internet of Things

Authors
Proença, J; Baquero, C;

Publication
Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers

Abstract
The reactive paradigm recently became very popular in user-interface development: updates — such as the ones from the mouse, keyboard, or from the network — can trigger a chain of computations organised in a dependency graph, letting the underlying engine control the scheduling of these computations. In the context of the Internet of Things (IoT), typical applications deploy components in distributed nodes and link their interfaces, employing a publish-subscribe architecture. The paradigm for Distributed Reactive Programming marries these two concepts, treating each distributed component as a reactive computation. However, existing approaches either require expensive synchronisation mechanisms or they do not support pipelining, i.e., allowing multiple “waves” of updates to be executed in parallel. We propose Quarp (Quality-Aware Reactive Programming), a scalable and light-weight mechanism aimed at the IoT to orchestrate components triggered by updates of data-producing components or of aggregating components. This mechanism appends meta-information to messages between components capturing the context of the data, used to dynamically monitor and guarantee useful properties of the dynamic applications. These include the so-called glitch freedom, time synchronisation, and geographical proximity. We formalise Quarp using a simple operational semantics, provide concrete examples of useful instances of contexts, and situate our approach in the realm of distributed reactive programming. © 2017, IFIP International Federation for Information Processing.

2017

Typed connector families and their semantics

Authors
Proença, J; Clarke, D;

Publication
Sci. Comput. Program.

Abstract