Recent Publications

Macedo N, Cunha A, Guimarães T.  2015.  Exploring Scenario Exploration. Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering. Abstractfase15var.pdf

Model finders are very popular for exploring scenarios, helping users validate specifications by navigating through conforming model instances. To be practical, the semantics of such scenario exploration operations should be formally defined and, ideally, controlled by the users, so that they are able to quickly reach interesting scenarios.
This paper explores the landscape of scenario exploration operations, by formalizing them with a relational model finder. Several scenario exploration operations provided by existing tools are formalized, and new ones are proposed, namely to allow the user to easily explore very similar (or different) scenarios, by attaching preferences to model elements. As a proof-of-concept, such operations were implemented in the popular Alloy Analyzer, further increasing its usefulness for (user-guided) scenario exploration.

Lamas J, Silva CC, Silva M, Mouta S, Campos JC, Santos J.  2015.  Measuring end-to-end delay in real-time auralisation systems. Euronoise – 10th European Congress and Exposition on Noise Control Engineering Abstractend2enddelay_euronoise2015.pdf

One of the major challenges in the development of an immersive system is handling the delay between the tracking of the user’s head position and the updated projection of a 3D image or auralised sound, also called end-to-end delay. Excessive end-to-end delay can result in the general decrement of the “feeling of presence”, the occurrence of motion sickness and poor performance in perception-action tasks. These latencies must be known in order to provide insights on the technological (hardware/software optimization) or psychophysical (recalibration sessions) strategies to deal with them. Our goal was to develop a new measurement method of end-to-end delay that is both precise and easily replicated. We used a Head and Torso simulator (HATS) as an auditory signal sensor, a fast response photo-sensor to detect a visual stimulus response from a Motion Capture System, and a voltage input trigger as real-time event. The HATS was mounted in a turntable which allowed us to precisely change the 3D sound relative to the head position. When the virtual sound source was at 90º azimuth, the correspondent HRTF would set all the intensity values to zero, at the same time a trigger would register the real-time event of turning the HATS 90º azimuth. Furthermore, with the HATS turned 90º to the left, the motion capture marker visualization would fell exactly in the photo-sensor receptor. This method allowed us to precisely measure the delay from tracking to displaying. Moreover, our results show that the method of tracking, its tracking frequency, and the rendering of the sound reflections are the main predictors of end-to-end delay.

Moreno CB, Lima R, Miranda H.  2015.  Adaptive Broadcast Cancellation Query Mechanism for Unstructured Networks. 9th International Conference on Next Generation Mobile Applications, Services and Technologies. Abstract142629213215577.pdf

The availability of cheap embedded sensors in mobile devices boosted the emergence of unstructured networks using wireless technologies without centralised administration. However, a simple task such as collecting temperature needs a discovery service to find a thermometer. Usually, the resource discovery relies on flooding mechanisms, wasting energy and compromising system availability. On the other hand, energy efficient solutions based on broadcast cancellation mechanism have a significant impact on latency. The paper proposes ABC (Adaptive Broadcast Cancellation) a new algorithm that uses the knowledge acquired in the past to accelerate queries towards the resource. Each node listens to its neighbours and the acquired context is stored in a variation of bloom filters.

Lima R, Moreno CB, Miranda H.  2015.  FBL - Filtro Bloom Linear. Infórum 2015. Abstractlima15.pdf

As estruturas de dados que permitem o armazenamento de informação de forma probabilística (em particular, os filtros de Bloom) caracterizam-se por permitir a regulação do equilíbrio entre a eficiência na gestão do espaço de armazenamento e a precisão das respostas. Esta possibilidade tem motivado a sua utilização em cenários adversos, por exemplo em redes de sensores, onde os dispositivos apresentam recursos limitados (memória, cpu, energia). Este artigo apresenta um mecanismo de Filtro de Bloom Linear (FBL), que permite associar a cada um dos elementos uma probabilidade quantizada no intervalo real [0,1], ultrapassando as limitações impostas pela característica binária dos filtros de Bloom. Os resultados mostram que é possível parametrizar um FBL de modo a manter um erro aceitável em função da variação do número de bits usados na quantização e do número de funções de hash usadas na indexação. O artigo discute a aplicação dos FBLs em mecanismos de disseminação e descoberta de recursos em redes de sensores, mostrando como contribuem para manter uma dimensão constante das mensagens trocadas pelos sensores, independentemente da dimensão da rede.

Oliveira R, Matos M, Felber P, Sutra P, Rivière E, Schiavoni V.  2015.  TOPiCo: detecting most frequent items from multiple high-rate event streams. DEBS 2015 - . Abstractp58-schiavoni.pdf

Systems such as social networks, search engines or trading platforms operate geographically distant sites that continuously generate streams of events at high-rate. Such events can be access logs to web servers, feeds of messages from participants of a social network, or financial data, among others. The ability to timely detect trends and popularity variations is of paramount importance in such systems. In particular, determining what are the most popular events across all sites allows to capture the most relevant information in near real-time and quickly adapt the system to the load. This paper presents TOPiCo, a protocol that computes the most popular events across geo-distributed sites in a low cost, bandwidth-efficient and timely manner. TOPiCo starts by building the set of most popular events locally at each site. Then, it disseminates only events that have a chance to be among the most popular ones across all sites, significantly reducing the required bandwidth. We give a correctness proof of our algorithm and evaluate TOPiCo using a real-world trace of more than 240 million events spread across 32 sites. Our empirical results shows that (i) TOPiCo is timely and cost-efficient for detecting popular events in a large-scale setting, (ii) it adapts dynamically to the distribution of the events, and (iii) our protocol is particularly efficient for skewed distributions.

Almeida D, Campos JC, Saraiva JA, Silva JC.  2015.  Towards a catalog of usability smells. SAC - Proceedings of the 30th Annual ACM Symposium on Applied Computing. Abstractsac2015_1.pdf

This paper presents a catalog of smells in the context of interactive applications. These so-called usability smells are indicators of poor design on an application's user interface, with the potential to hinder not only its usability but also its maintenance and evolution. To eliminate such usability smells we discuss a set of program/usability refactorings. In order to validate the presented usability smells catalog, and the associated refactorings, we present a preliminary empirical study with software developers in the context of a real open source hospital management application. Moreover, a tool that computes graphical user interface behavior models, giving the applications' source code, is used to automatically detect usability smells at the model level.

Abreu R, Passos LS, Rossetti RJF.  2015.  Spectrum-Based Fault Localisation for Multi-Agent Systems. IJCAI - 24th International Joint Conference on Artificial Intelligence. Abstractijcai15-164.pdf

Diagnosing unwanted behaviour in Multi-Agent Systems (MASs) is crucial to ascertain agents’ correct operation. However, generation of MAS models is both error-prone and time intense, as it exponentially increases with the number of agents and their interactions. In this paper, we propose a light-weight, automatic debugging-based technique, coined ESFL-MAS, which shortens the diagnostic process, while only relying on minimal information about the system. ESFL-MAS uses a heuristic that quantifies the suspiciousness of an agent to be faulty; therefore, different heuristics may have different impact on the diagnostic quality. Our experimental evaluation shows that 10 out of 42 heuristics yield the best diagnostic accuracy (96.26% on average).

Masci P, Oladimeji P, Zhang Y, Jones P, Curzon P, Thimbleby H.  2015.  PVSio-web 2.0: Joining PVS to Human-Computer Interaction. 27th International Conference on Computer Aided Verification (CAV2015). Abstractpvsioweb-cav2015.pdf

PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users.

This paper presents the latest release of PVSio-web 2.0, which will be part of the next PVS distribution. The new tool architecture is discussed, and the rationale behind its design choices are presented

Masci P, Couto LD, Larsen PG, Curzon P.  2015.  Integrating the PVSio-web modelling and prototyping environment with Overture. 13th Overture Workshop, satellite event of FM2015. Abstractpvsioweb-overture2015.pdf

Tools are needed that overcome the barriers preventing development teams using formal verification technologies. We present our work integrating PVSio-web with the Overture development and analysis environment for VDM. PVSio-web is a graphical environment for modelling and prototyping interactive systems. Prototypes developed within PVSio-web can closely resemble the visual appearance and behaviour of a real system. The behaviour of the prototypes is entirely driven by executable formal models. These formal models can be generated automatically from Emucharts, graphical diagrams based on the Statechart notation. Emucharts conveniently hides aspects of the formal syntax that create barriers for developers and domain experts who are new to formal methods. Here, we present the implementation of a VDM-SL model generator for Emucharts. An example is presented based on a medical device. It demonstrates the benefits of using Emucharts to develop a formal model, how PVSio-web can be used to perform lightweight formal analysis, and how the developed VDM-SL model generator can be used to produce a model that can be further analysed within Overture.

Masci P, Mallozzi P, DeAngelis FL, Serugendo GDM, Curzon P.  2015.  Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments. Verisure2015, Workshop on Verification and Assurance, co-located with CAV2015. Abstractpvsioweb-sapere-verisure2015.pdf

Integrated clinical environments (ICEs) consist of interoperable medical devices that seamlessly exchange data and commands to create safety interlocks and closed loop controls to improve the quality of care delivered to the patient. Currently at the prototype stage, they promise to form the basis of a new generation of healthcare systems for high acuity patients. Regulators such as the US Food and Drug Administration are promoting the development of tools and techniques for verification and validation of essential safety requirements for ICEs. To date, little research has focused on the certification and assurance of their user interfaces with respect to use errors. In this work, we demonstrate how the PVSio-web prototyping tool can be conveniently used in combination with the communication framework SAPERE to generate realistic ICE systems prototypes from formal models. This approach is particularly suitable for exploring requirements, design, and regulatory issues of usability and safety of the user interfaces of ICE systems. An example ICE system prototype is presented, along with an example analysis demonstrating how the prototype can be used to explore subtle user interface design issues that could lead to usability and safety hazards in clinical scenarios.

Neves F, Pereira JO, Vilaça R, Oliveira R.  2015.  Otimização do HBase para dados estruturados. INForum 2015. :235-247. Abstractpscan.pdf

Os sistemas NoSQL escalam melhor que os tradicionais sistemas relacionais, motivando a migração de inúmeras aplicações para sistemas NoSQL mesmo quando não se tira partido da estrutura de dados dinâmica por eles fornecida. Porém, a consulta destes dados estruturados tem um custo adicional que deriva da flexibilidade dos sistemas NoSQL. Neste documento, analisa-se esse custo no Apache HBase e apresenta-se o Prepared Scan, uma operação adicional de consulta que visa tirar partido do conhecimento da estrutura de dados por parte da aplicação, diminuindo assim o custo associado à consulta de dados estruturados. Recorrendo à ferramenta de benchmarking YCSB, verifica-se que esta solução tem um aumento no débito de aproximadamente 29%.

Pedro AM, Pereira D, Pinho LM, Pinto JS.  2015.  Monitoring for a Decidable Fragment of Mtl-∫. In Proceedings of Runtime Verification - 6Th International Conference, Rv 2015 . 9333 Abstract2015_rv_15.pdf

Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-∫, we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

Machado M, Campos JC, Couto R.  2015.  MODUS: uma metodologia de prototipagem de interfaces baseada em modelos. Inforum 2015: Atas do 7º Simpósio Nacional de Informática. :17-32.inforum-2015.pdf
Masci P, Oladimeji P, Mallozzi P, Curzon P, Thimbleby H.  2015.  PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". Abstractmobihealth-pvsioweb.pdf

Use errors, where medical devices work to specification but lead to the clinicians making mistakes resulting in patient harm, is a critical problem. Manufacturers need tools to help them find such design flaws at an early stage and regulators need tools to help check devices are safe to approve for market. We have developed a prototyping tool, PVSio-web, to help check the safety of medical device interface and interaction design. It supports a model-based design process: that is, it is based on precise mathematical descriptions of the device's behaviour. This allows sophisticated proof and model checking technology to be used to verify that devices meet essential safety requirements. The architecture allows for the flexible addition of `plug-in' modules to extend its functionality giving different views of the design that allow different stakeholders to work together. Working with the US regulator, the Food and Drug Administration (FDA), our tool has helped identify problems in a series of commercial medical devices. Hospitals have used it as part of training programmes highlighting safety-related design issues. In ongoing work we are developing plug-ins that support the verification and validation of interoperable medical systems.