Recent Publications

Barbosa LS.  2005.  A Perspective on Component Refinement. Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 - 5, 2004, Revised Lectures. 3657:23–48. Abstract

This paper provides an overview of an approach to coalgebraic modelling and refinement of state-based software components, summing up some basic results and introducing a discussion on the interplay between behavioural and classical data refinement. The approach builds on coalgebra theory as a suitable tool to capture observational semantics and to base an abstract characterisation of possible behaviour models for components (from partiality to different degrees of non-determinism).

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.

Cledou G, Barbosa L.  Submitted.  Modeling Families of Public Licensing Services: A Case Study. FME Workshop on Formal Methods in Software Engineering (FormaliSE). formalise2017.pdf
Neves F, Vilaça R, Pereira JO, Oliveira R.  Submitted.  Prepared Scan: Efficient Retrieval of Structured Data from HBase. {Proceedings of the Symposium on Applied Computing, Sac 2017, Marrakech, Morocco, April 3-7, 2017}. {Part F128005}:{462-464}. Abstractp462-neves.pdf

n/a

Bernardeschi C, Masci P, Santone A.  2018.  Data Leakage in Java applets with Exception Mechanism. Proceedings of Italian Conference on Cyber-Security (ITASEC18). CEUR Workshop Proceedings (2018, to appear)santone.pdf
Neves F, Machado N, Pereira JO.  2018.  Falcon: A Practical Log-based Analysis Tool for Distributed Systems. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN’18).
Bernardeschi C, Masci P, Caramella D, Dell'Osso R.  2018.  The benefits of using interactive device simulations as training material for clinicians: an experience report with a contrast media injector used in CT. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)stellant-v3.pdf
Silva CC, Masci P, Zhang Y, Jones P, Campos JC.  2018.  A Use Error Taxonomy for Improving Human-Machine Interface Design in Medical Devices. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)mcps-taxonomy-v3g.pdf
Ribeiro J, Machado N, Maia F, Matos M.  2018.  Totally Ordered Replication for Massive Scale Key-Value Stores. 18th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS'18).
Broccia G, Masci P, Milazzo P.  2018.  Modeling and Analysis of Human Memory Load in Multitasking Scenarios. 10th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2018). Abstract

This paper presents on-going work developing a formal framework for the model-based analysis of human-machine interaction in multiple critical systems. The framework builds on classical results from applied psychology on selective attention and working memory. The framework is intended for developers of interactive critical systems to identify plausible human multitasking strategies that are likely to be adopted by operators when using multiple interactive systems at the same time, and to estimate the memory load necessary to complete concurrent tasks. This type of analysis is especially useful at the early stages of system design, to better understand the effort necessary to operate the system when an implementation or a prototype of the system is unavailable. The analysis can also be used retrospectively, to analyse already implemented systems and complement results from user studies. An example based on infusion pumps, used in chemotherapy to infuse doses over a period, is employed to demonstrate the utility of the framework. The framework makes it possible to model the interactive tasks necessary to configure the pumps and start the infusion. The results of the analysis indicate situations where the operator is unable to carry out the task because of omission errors. These results are in line with experimental results reported in the literature, and may provide more detailed hypotheses that can be validated experimentally.