Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About
Download Photo HD

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
  • Role

    External Research Collaborator
  • Since

    01st March 2013
  • Nationality

    Portugal
  • Contacts

    +351253604440
    jose.p.proenca@inesctec.pt
003
Publications

2020

ARx: Reactive Programming for Synchronous Connectors

Authors
Proença, J; Cledou, G;

Publication
Lecture Notes in Computer Science - Coordination Models and Languages

Abstract

2019

Coordination of tasks on a real-time OS

Authors
Cledou, G; Proenca, J; Sputh, BHC; Verhulst, E;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
VirtuosoNext TM is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel as a kind of Guarded Protected Action with a well defined semantics. While the kernel provides the most basic services, each carefully designed, tested and optimised, tasks are limited to this handful of basic hubs, leaving the development of more complex synchronization and communication mechanisms up to application specific implementations. In this work we investigate how to support a programming paradigm to compositionally build new services, using notions borrowed from the Reo coordination language, and relieving tasks from coordination aspects while delegating them to the hubs. We formalise the semantics of hubs using an automata model, identify the behaviour of existing hubs, and propose an approach to build new hubs by composing simpler ones. We also provide tools and methods to analyse and simplify hubs under our automata interpretation. In a first experiment several hub interactions are combined into a single more complex hub, which raises the level of abstraction and contributes to a higher productivity for the programmer. Finally, we investigate the impact on the performance by comparing different implementations on an embedded board. © IFIP International Federation for Information Processing 2019.

2019

Taming Hierarchical Connectors

Authors
Proença, J; Madeira, A;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas. © 2019, IFIP International Federation for Information Processing.

2019

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

Authors
Monahan, R; Prevosto, V; Proença, J;

Publication
F-IDE@FM

Abstract

2018

Teaching how to program using automated assessment and functional glossy games (experience report)

Authors
Almeida, JB; Cunha, A; Macedo, N; Pacheco, H; Proenca, J;

Publication
Proceedings of the ACM on Programming Languages

Abstract