Conference Papers

Fayollas C, Martinie C, Palanque P, Masci P, Harrison M, Campos JC, Silva SR.  2017.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Proceedings of the Third Workshop on Formal Integrated Development Environment. 240:1-19. Abstract1701.08465.pdf


Masci P, Zhang Y, Jones P, Campos JC.  2017.  A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices. 15th International Conference on Software Engineering and Formal Methods (SEFM 2017). LNCS, volume 10469, Springer Abstractsefm17-cameraready.pdf

Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson's System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that 1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and 2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).

Harrison MD, Drinnan M, Campos JC, Masci P, Freitas L, Di Maria C, Whitaker M.  2017.  Safety analysis of software components of a dialysis machine using model checking. 14th International Conference on Formal Aspects of Component Software. Abstractpaper_7.pdf

The paper describes the practical use of a model checking technique to contribute to the risk analysis of a new paediatric dialysis machine. The formal analysis focuses on one component of the system, namely the table-driven software controller which drives the dialysis cycle and deals with error management. The analysis provided evidence of the verification of risk control measures relating to the software component. The paper describes the productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and an analyst who had experience of using the formal analysis tools. There were two aspects to this dialogue. The first concerned the translation of safety requirements so that they preserved the meaning of the requirement. The second involved understanding the relationship between the software component under analysis and the broader concern of the system as a whole. The paper focuses on the process, highlighting how the team recognised the advantages over a more traditional testing approach.

Pinto M, Goncalves M, Masci P, Campos JC.  2017.  TOM: a Model-Based GUI Testing framework. 14th International Conference on Formal Aspects of Component Software. Abstractpaper_25.pdf

Applying model-based testing to interactive systems enables the systematic testing of the system by automatically simulating user actions on the user interface. It reduces the cost of (expensive) user testing by identifying implementations errors without the involvement of human users, but raises a number of specific challenges, such as how to achieve good coverage of the actual use of the system during the testing process. This paper describes TOM, a model-based testing framework that uses a combination of tools and mutation testing techniques to maximize testing of user interface behaviors

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.

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.

Abade T, Campos JC, Moreira R, Silva CC, Silva JL.  2015.  Immersiveness of Ubiquitous Computing Environments Prototypes: A case study. Lecture Notes in Computer Science. 9189 Abstract15-dapi-abadecmss-sarch.pdf

The development of ubiquitous computing (ubicomp) environments raises several challenges in terms of their evaluation. Ubicomp virtual reality prototyping tools enable users to experience the system to be developed and are of great help to face those challenges, as they support developers in assessing the consequences of a design decision in the early phases of development. Given the situated nature of ubicomp environments, a particular issue to consider is the level of realism provided by the prototypes. This work presents a case study where two ubicomp prototypes, featuring different levels of immersion (desktop-based versus CAVE-based), were developed and compared. The goal was to determine the cost/benefits relation of both solutions, which provided better user experience results, and whether or not simpler solutions provide the same user experience results as more elaborate one.

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.

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.

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
Harrison M, Campos J, Masci P, Curzon P.  2015.  Templates as heuristics for proving properties of medical devices. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". antennatemplatesv5-final.pdf
Campos JC, Silva JL, Harrison M.  2015.  Supporting the Design of an Ambient Assisted Living System Using Virtual Reality Prototypes. Ambient Assisted Living. ICT-based Solutions in Real Life Situations. 9455:49-61.authorsversion.pdf
Sousa M, Campos JC, Alves M, Harrison M.  2014.  Formal Verification of Safety-Critical User Interfaces: a space system case study. Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium. :62-67. Abstract7722-34384-1-pb.pdf

Safe operation of safety critical systems depends on appropriate interactions between the human operator and the computer system. Specification of such safety-critical systems is fundamental to enable exhaustive and automated analysis of operator system interaction. In this paper we present a structured, comprehensive and computer-aided approach to formally specify and verify user interfaces based on model checking techniques.

Couto R, Ribeiro AN, Campos JC.  2014.  Application of Ontologies in Identifying Requirements Patterns in Use Cases. 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA. 147:62–76. Abstractfesca_2014.pdf

Use case specifications have successfully been used for requirements description. They allow joining, in the same modeling space, the expectations of the stakeholders as well as the needs of the software engineer and analyst involved in the process. While use cases are not meant to describe a system's implementation, by formalizing their description we are able to extract implementation relevant information from them. More specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. In the paper we propose the transformation of Use Case descriptions expressed in a Controlled Natural Language into an ontology expressed in the Web Ontology Language (OWL). OWL's query engines can then be used to identify requirements patterns expressed as queries over the ontology. We describe a tool that we have developed to support the approach and provide an example of usage.

Campos JC, Arcuri A, Fraser G, Abreu R.  2014.  Continuous Test Generation: Enhancing Continuous Integration with Automated Test Generation. Proceedings Automated Software Engineering (ASE). Abstractase14_ctg.pdf

In object oriented software development, automated unit test generation tools typically target one class at a time. A class, however, is usually part of a software project consisting of more than one class, and these are subject to changes over time. This context of a class offers significant potential to improve test generation for individual classes. In this paper, we introduce Continuous Test Generation (CTG), which includes automated unit test generation during continuous integration (i.e., infrastructure that regularly builds and tests software projects). CTG offers several benefits: First, it answers the question of how much time to spend on each class in a project. Second, it helps to decide in which order to test them. Finally, it answers the question of which classes should be subjected to test generation in the first place. We have implemented CTG using the EVOUITE unit test generation tool, and performed experiments using eight of the most popular open source projects available on GitHub, ten randomly selected projects from the SF100 corpus, and five industrial projects. Our experiments demonstrate improvements of up to +58% for branch coverage and up to +69% for thrown undeclared exceptions, while reducing the time spent on test generation by up to +83%.

Couto R, Ribeiro AN, Campos JC.  2014.  The Modelery: A Collaborative Web Based Repository. 14th International Conference on Computational Science and Its Applications (ICCSA 2014). 8584 Abstracticcsa_2014.pdf

Software development processes are known to produce a large set of artifacts such as models, code and documentation. Keeping track of these artifacts without supporting tools is not easy, and making them available to others can be even harder. Standard version control systems are not able to solve this issue. More than keeping track of versions, a system to help organize and make artifacts available in meaningful ways is needed. In this paper we review a number of alternative systems, and present the requirements and the implementation of a collaborative web repository which we developed to solve this issue.

Couto R, Ribeiro AN, Campos JC.  2014.  A study on the viability of formalizing Use Cases. 9th International Conference on the Quality of Information and Communications Technology (QUATIC). Abstract6133a130.pdf

Use case scenarios are known as powerful meansfor requirements specification. On th e one hand, they join in the same modeling space the expectations of the stakeholders and the needs of the developers involved in the process. On the other hand, they describe the desired high level functionalities. By formalizing these descriptions we are able to extract relevant informations from them. Specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. This paper addresses the transformation of use case descriptions expressed in a Controller Natural Language into an ontology expressed in the Web Ontology Language (OWL), as well as the query process for such information. It reports on a study aimed at validating our approach and our tool with real users. A preliminary set of results is discussed.

Silva CE, Campos JC.  2014.  Characterizing the Control Logic of Web Applications' User Interfaces. In Computational Science and Its Applications - ICCSA 2014. 8584:263–276. Abstracticcsa_final.pdf

On order to develop an hybrid approach to the Reverse Engineer of Web applications, we need rst to understand how much of the control logic of the user interface can be obtained from the analysis of event listeners. To that end, we have developed a tool that enables us to perform such analysis, and applied it to the implementation of the one thousand most widely used Websites (according to Alexa Top Sites). This paper describes our approach for analyzing the user interface layer of those Websites, and the results we got from the analysis. The conclusions drawn from the exercise will be used to guide the development of the proposed hybrid reverse engineering tool.

Campos JC, Silva JL, Abade T, Gomes T.  2014.  Design and Evaluation of a Smart Library using the APEX Framework. Distributed, Ambient, and Pervasive Interactions. 8530 Abstract2014-hcii-dapi.pdf

User experience is a key point for successful ubiquitous computing (ubicomp) environments. The envisaged design should be explored as soon as possible to anticipate potential user problems, thus reducing re-design costs. The development of ubicomp environments’ prototypes might help, providing feedback on the users’ reaction to the environments. This paper describes the design and evaluation of ubicomp environments using APEX, a rapid prototyping framework providing user experience via a 3D application server and connected physical devices. APEX prototypes allow users to explore and experience many characteristics of a proposed design, in a virtual world. The paper focus in particular the design and evaluation of a smart library in the APEX framework.

Campos JC, AI S.  2014.  Towards a Framework for Adaptive Web Applications. HCI International 2014 - Posters' Extended Abstracts. 434 Abstract2014-hcii-as.pdf

We have developed a framework to support adaptive elements in Web pages. In particular we focus on adaptive menus. Developers are able to define rules for menu adaptation according to the features of the device and browser in use. This paper briefly describes the selected adaptation patterns and their implementation.

Campos JC, Abade T, Gomes T, Harrison M, Silva JL.  2014.  Rapid Development of First Person Serious Games using the APEX Platform: The Asthma Game. Proceedings of ACM SAC 2014 . 1 Abstract2014-sac.pdf

Serious games combine a ludic component with instructive and formative goals. They aim to educate and train through play. This paper explores the use of a development framework for dynamic virtual environments to develop serious games. The framework (APEX) was originally developed to prototype ubiquitous computing environments. Here it is used to develop a first person serious game: the Asthma Game. This game aims to teach children with asthma how to act to prevent attacks by drawing attention to asthma triggers in the home, and by providing information about how to avoid them. Besides the description of the game, results about the viability and utility of the approach are also discussed.

Campos JC.  2014.  High assurance interactive computing systems. HCI Engineering: Charting the Way towards Methods and Tools for Advanced Interactive Systems. Abstractcampos.pdf

If interactive computing systems development is to be considered an engineering discipline, we need methods and tools to help us reason about and predict the quality of systems, from early in the design process. This paper provides a brief overview of work we have been carrying out in the general area of evaluating and ensuring the quality of interactive computing systems. Some of the work currently being carried out is also discussed. Discussed approaches range from the formal verification of user interface models through model checking, to the reverse engineering and model based testing of implemented interactive computing systems.

Campos JC, Silva JC, Silva JL, Saraiva JA.  2014.  An approach for graphical user interface external bad smells detection. Advances in Intelligent Systems and Computing. 276 Abstract

In the context of an effort to develop methodologies to support the evaluation of interactive system, this paper investigates an approach to detect graphical user interface external bad smells. Our approach consists in detecting user interface external bad smells through model-based reverse engineering from source code. Models are used to define which widgets are present in the interface, when can particular graphical user interface (GUI) events occur, under which conditions, which system actions are executed, and which GUI state is generated next. From these models we obtain metrics that can later be used to identify the smells.

Harrison M, Masci P, Campos JC, Curzon P.  2014.  Demonstrating that medical devices satisfy user related safety requirements. FHIES/SEHC - Fourth Symposium on Foundations of Health Information Engineering and Systems (FHIES) and the Software Engineering in Healthcare (SEHC) - post-proceedings. Abstractharrison-fhies14.pdf

One way of contributing to a demonstration that a medical device is acceptably safe is to show that the device satisfies a set of requirements known to mitigate hazards. This paper describes experience using formal techniques to model an IV infusion device and to prove that the modelled device captures a set of requirements. The requirements chosen for the study are based on a draft proposal developed by the US Food and Drug Administration (FDA). A major contributor to device related errors are (user) interaction errors. For this reason the chosen models and requirements focus on user interface related issues.