Recent Publications

Ferreira JF, Sobral JL.  2005.  ParC#: Parallel Computing with C# in .NET. Parallel Computing Technologies (LNCS 3606). Abstract

This paper describes experiments with the development of a parallel computing platform on top of a compatible C# implementation: the Mono project. This implementation has the advantage of running on both Windows and UNIX platforms and has reached a stable state. This paper presents performance results obtained and compares these results with implementations in Java/RMI. The results show that the Mono network performance, critical for parallel applications, has greatly improved in recent releases, that it is superior to the Java RMI and is close to the performance of the new Java nio package. The Mono virtual machine is not yet so highly tuned as the Sun JVM and Thread scheduling needs to be improved. Overall, this platform is a new alternative to explore in the future for parallel computing.

Oliveira JN, Rodrigues C.  2004.  Transposing Relations: from Maybe Functions to Hash Tables. MPC - 7th International Conference on Mathematics of Program Construction. 3125:334-356. Abstract

Functional transposition is a technique for converting relations into functions aimed at developing the relational algebra via the algebra of functions. This paper attempts to develop a basis for generic transposition. Two instances of this construction are considered, one applicable to any relation and the other applicable to simple relations only. Our illustration of the usefulness of the generic transpose takes advantage of the free theorem of a polymorphic function. We show how to derive laws of relational combinators as free theorems of their transposes. Finally, we relate the topic of functional transposition with the hashing technique for efficient data representation.

Pereira JO, Rodrigues L, Oliveira R.  2002.  Semantically Reliable Broadcast: Sustaining High Throughput in Reliable Distributed Systems. Concurrency in Dependable Computing. Abstract

Replicated services are often required to sustain high loads of multiple concurrent requests. This requirement is hard to balance with strong consistency. Typically, to ensure inter-replica consistency, all replicas should receive all updates. Unfortunately, in this case, a single slow replica may degrade the performance of the whole system. This paper proposes a novel reliable broadcast primitive that uses semantic knowledge to weaken reliable delivery guarantees while, at the same time, ensuring strong consistency at the semantic level. By allowing some obsolete messages to be dropped, the protocol that implements this primitive is able to sustain a higher throughput than a fully reliable broadcast protocol. The usefulness of the primitive and the performance of the protocol are illustrated through a concrete example.

Noble J, Vitek J, Lea D, Almeida PS.  1999.  Aliasing in object oriented systems. Object-Oriented Technology ECOOP’99 Workshop Reader. :793–793. Abstract

This chapter contains summaries of the presentations given at the Intercontinental Workshop on Aliasing in Object-Oriented Systems (IWAOOS’99) at the European Conference on Object-Oriented Programming (ECOOP’99) which was held in Lisbon, Portugal on June 15, 1999.

Almeida PS.  1997.  Balloon types: Controlling sharing of state in data types. ECOOP'97—Object-Oriented Programming. :32–59. Abstract

Current data abstraction mechanisms are not adequate to control sharing of state in the general case involving objects in linked structures. The pervading possibility of sharing is a source of errors and an obstacle to language implementation techniques.
We present a general extension to programming languages which makes the ability to share state a first class property of a data type, resolving a long-standing flaw in existing data abstraction mechanisms.
Balloon types enforce a strong form of encapsulation: no state reachable (directly or transitively) by a balloon object is referenced by any external object. Syntactic simplicity is achieved by relying on a non-trivial static analysis as the checking mechanism.
Balloon types are applicable in a wide range of areas such as program transformation, memory management and distributed systems. They are the key to obtaining self-contained composite objects, truly opaque data abstractions and value types—important concepts for the development of large scale, provably correct programs.

He M, Vafeiadis V, Qin S, Ferreira JF.  2016.  Reasoning about Fences and Relaxed Atomics. Search Results 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. Abstract2016-pdp-gpsfences.pdf

For efficiency reasons, weak (or relaxed) memory is now the norm on modern architectures. To cater for this trend, modern programming languages are adapting their memory models. The new C11 memory model allows several levels of memory weakening, including non-atomics, relaxed atomics, release-acquire atomics, and sequentially consistent atomics. Under such weak memory models, multithreaded programs exhibit more behaviours, some of which would have been inconsistent under the traditional strong (i.e. sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, recently developed by Turon et al., has made a step forward towards tackling this challenge. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we present a program logic, an enhancement of the GPS framework, that can support the verification of a bigger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of newly-designed verification rules.

Even C, Bosser A-G, Ferreira JF, Buche C, Stéphan F, Cavazza M, Lisetti C.  2016.  Supporting Social Skills Rehabilitation with Virtual Storytelling. 29th International FLAIRS Conference. Abstract12953-57659-1-pb.pdf

Social skills training (SST) has recently emerged as a typical application for emotional conversational agents (ECA). While a number of prototypes have targeted the general population, fewer have been used for psychiatric patients despite the widely recognised potential of ECAs technologies in the field of mental health. Social cognition impairment is however a widely shared symptom in psychiatric patients suffering from pathologies such as schizophrenia. Going further than SST, rehabilitation programmes involving role-play, but also problem solving have been successfully used by clinicians, drastically improving the quality of life of patients suffering from such disabilities. One of the challenges of these programmes is to ensure that the patients will be able to adapt their behaviour when the situation varies, rather than training them with the appropriate behaviour for a set of specific situations.
In this paper, we describe a novel approach for the development of a serious game supporting rehabilitation programmes for social skills, which will primarily target schizophrenia patients. We propose to use an ECA in combination with a narrative generation engine issued from interactive storytelling research to provide varied situations. This approach reflects the combination of both role-play and problem solving exercises on which remediation therapies rely, and has the potential to support patient's progress and motivation through the rehabilitation programme.

Couto R, Ribeiro AN, Campos JC.  2016.  Validating an approach to formalize use cases with ontologies. Proceedings of the 13th International Workshop on Formal Engineering Approaches to Software Components and Architectures. 205:1-15. Abstract1603.08632v1.pdf

Use case driven development methodologies put use cases at the center of the software development process. However, in order to support automated development and analysis, use cases need to be appropriately formalized. This will also help guarantee consistency between requirements specifications and the developed solutions. Formal methods tend to suffer from take up issues, as they are usually hard to accept by industry. In this context, it is relevant not only to produce languages and approaches to support formalization, but also to perform their validation. In previous works we have developed an approach to formalize use cases resorting to ontologies. In this paper we present the validation of one such approach. Through a three stage study, we evaluate the acceptance of the language and supporting tool. The first stage focusses on the acceptance of the process and language, the second on the support the tool provides to the process, and finally the third one on the tool's usability aspects. Results show test subjects found the approach feasible and useful and the tool easy to use.

Moreno CB, Almeida PS, Lerche C.  2016.  The problem with embedded CRDT counters and a solution. PaPoC '16 Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data. abstractcounterpapocfinal.pdf
Zawirski M, Moreno CB, Zawirski M, Preguiça N, Shapiro M.  2016.  Eventually Consistent Register Revisited. Proceeding PaPoC '16 Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data. mvreg_papoc_camera.pdf
Campos JC, Fayollas C, Martinie C, Navarre D, Palanque P, Pinto M.  2016.  Systematic Automation of Scenario-Based Testing of User Interfaces. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 138-148. Abstractfp0148-paper.pdf

Ensuring the effectiveness factor of usability consists in ensuring that the application allows users to reach their goals and perform their tasks. One of the few means for reaching this goal relies on task analysis and proving the compatibility between the interactive application and its task models. Synergistic execution enables the validation of a system against its task model by co-executing the system and the task model and comparing the behavior of the system against what is prescribed in the model. This allows a tester to explore scenarios in order to detect deviations between the two behaviors. Manual exploration of scenarios does not guarantee a good coverage of the analysis. To address this, we resort to model-based testing (MBT) techniques to automatically generate scenarios for automated synergistic execution. To achieve this, we generate, from the task model, scenarios to be co-executed over the task model and the system. During this generation step we explore the possibility of including considerations about user error in the analysis. The automation of the execution of the scenarios closes the process. We illustrate the approach with an example.

Harrison M, Campos JC, Ruksenas R, Curzon P.  2016.  Modelling information resources and their salience in medical device design. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 194-203. Abstractocbeics16pub.pdf

The paper describes a model that includes an explicit description of the information resources that are assumed to guide use, enabling a focus on properties of "plausible interactions". The information resources supported by an interactive system should be designed to encourage the correct use of the system. These resources signpost a user's interaction, helping to achieve desired goals. Analysing assumptions about information resource support is particularly relevant when a system is safety critical that is when interaction failure consequences could be dangerous, or walk-up-and-use where interaction failure may lead to reluctance to use with expensive consequences. The paper shows that expressing these resource constraints still provides a wider set of behaviours than would occur in practice. A resource may be more or less salient at a particular stage of the interaction and as a result potentially overlooked. For example, the resource may be accessible but not used because it does not seem relevant to the current goal. The paper describes how the resource framework can be augmented with additional information about the salience of the assumed resources. A medical device that is in common use in many hospitals is used as illustration.

Bernardeschi C, Domenici A, Masci P.  2016.  Modeling Communication Network Requirements for an Integrated Clinical Environment in the Prototype Verification System. ICTS4eHealth - 1st IEEE Workshop on ICT solutions for eHealth. Abstractmasci-icts4ehealth-cr.pdf

Health care practices increasingly rely on complex technological infrastructure, and new approaches to the integration of information and communication technology in those practices lead to the development of such concepts as integrated clinical environments and smart intensive care units. These concepts refer to hospital settings where therapy relies heavily on inter-operating medical devices, supervised by clinicians assisted by advanced monitoring and coordinating software. In order to ensure safety and effectiveness of patient care, it is necessary to specify the requirements of such socio-technical systems in the most rigorous and precise way. This paper presents an approach to the formalization of system requirements for communication networks deployed in integrated clinical environment, based on the higher-order logic language of a theorem-proving environment, the Prototype Verification System. http://dx.doi.org/10.1109/ISCC.2016.7543728

Coelho F, Pereira JO, Vilaça R, Oliveira R.  2016.  Holistic Shuffler for the Parallel Processing of SQL Window Functions. Distributed Applications and Interoperable Systems - 16th {IFIP} {WG} 6.1 International Conference, {DAIS} 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June. :75–81. Abstractholistic-proceedings.pdf

Window functions are a sub-class of analytical operators that allow data to be handled in a derived view of a given relation, while taking into account their neighboring tuples. Currently, systems bypass parallelization opportunities which become especially relevant when considering Big Data as data is naturally partitioned.
We present a shuffling technique to improve the parallel execution of window functions when data is naturally partitioned when the query holds a partitioning clause that does not match the natural partitioning of the relation. We evaluated this technique with a non-cumulative ranking function and we were able to reduce data transfer among parallel workers in 85% when compared to a naive approach.

Coelho F, Pereira JO, Vilaça R, Oliveira R.  2016.  Reducing Data Transfer in Parallel Processing of SQL Window Functions. Proceedings of the 6th International Conference on Cloud Computing and Services Science. :343-347. Abstractdatadiversityconvergence_2016_1_copy.pdf

Window functions are a sub-class of analytical operators that allow data to be handled in a derived view of a given relation, while taking into account their neighboring tuples. We propose a technique that can be used in the parallel execution of this operator when data is naturally partitioned. The proposed method benefits the cases where the required partitioning is not the natural partitioning employed. Preliminary evaluation shows that we are able to limit data transfer among parallel workers to 14\% of the registered transfer when using a naive approach.