Journal Articles

Harrison M, Masci P, Campos JC.  2018.  Verification templates for the analysis of user interface software design. IEEE Transactions on Software Engineering (to appear). Abstractnewtemplates-r1v7b.pdf

The paper describes templates for model-based analysis of usability and safety aspects of user interface software design. The templates crystallize general usability principles commonly addressed in user-centred safety requirements, such as the ability to undo user actions, the visibility of operational modes, and the predictability of user interface behavior. These requirements have standard forms across different application domains, and can be instantiated as properties of specific devices. The modeling and analysis process is carried out using the Prototype Verification System (PVS), and is further facilitated by structuring the specification of the device using a format that is designed to be generic across interactive systems. A concrete case study based on a commercial infusion pump is used to illustrate the approach. A detailed presentation of the automated verification process using PVS shows how failed proof attempts provide precise information about problematic user interface software features.

Harrison MD, Masci P, Campos JC, Curzon P.  2017.  Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. IEEE Transactions on Human-Machine Systems. 47:834-846. Abstractmedthmsv9-author_version.pdf

One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: (i) how to validate a model, and show that it is a faithful representation of the device;
(ii) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; (iii) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based on US Food and Drug Administration (FDA) draft documentation
for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA’s agenda of using formal methods to support the approval process for medical devices.

Campos JC, Fayollas C, Gonçalves M, Martinie C, Navarre D, Palanque P, Pinto M.  2017.  A ``More Intelligent'' Test Case Generation Approach through Task Models Manipulation. Proceedings of the ACM on Human-Computer Interaction – EICS. 1:Article9. Abstractpacmhci-eics17-accepted.pdf

Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the effectiveness factor of usability directly refers to this capability. Assessing effectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of effectiveness of interactive applications. To this end we resort to two main elements: an exhaustive description of users’ activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance
(both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications.

Campos JC, Abade T, Silva JL, Harrison MD.  2017.  Don't Go In There! Using the APEX framework in the design of Ambient Assisted Living Systems. Journal of Ambient Intelligence and Humanized Computing. 8:551-566. Abstract17-jaihc-author-2.pdf

An approach to design Ambient Assisted Living systems is presented, which is based on APEX, a framework for prototyping ubiquitous environments. The approach is illustrated through the design of a smart environment within a care home for older people. Prototypes allow participants in the design process to experience the proposed design and enable developers to explore design alternatives rapidly. APEX provides the means to explore alternative environment designs virtually. The prototypes developed with APEX offered a mediating representation, allowing users to be involved in the design process. A group of residents in a city-based care home were involved in the design. The paper describes the design process as well as lessons learned for the future design of AAL systems.

Campos JC, Sousa M, Alves M, Harrison M.  2016.  Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems. 46(2):303-316. Abstractthms-paper-author_version.pdf

This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.

Couto R, Ribeiro AN, Campos JC.  2015.  The Modelery: A Model-Based Software Development Repository. International Journal of Web Information Systems. Abstractijwisv2.pdf

– This paper aims to present the Modelery, a platform for collaborative repository to support model-based software development. The Modelery is a Web platform, composed both by a Web page and Web services for interoperability.

– By performing a study in the existing platforms, it was possible to achieve a set of issues to tackle. The issues enabled the possibility to define a set of requirements that allowed the authors to design a new platform, and to perform a model-driven software development process, which started from the requirements until reaching the final software solution.

– With this work, it was possible to perform a survey on the currently available artifacts repositories, categorize them and identify their shortcomings. This was essential to define the set of requirements for a new platform to overcome the identified issues. This process leads to a platform able to improve the currently available solutions, and validated in the scientific community. In this paper, the authors also explore the applications of the repository. First, they use the Modelery to replace an older model’s repository. Second, they have enabled the communication between other tools and the Modelery via Web services.

– This work presents a new Web repository for software artifacts aimed at supporting researchers and software developers. The presented platform is an improvement over other platforms on the integration of artifacts repository, social functionalities and scientific publications integration. The authors conclude this paper by comparing the achieved platform in terms of functionalities, against the other analyzed platforms.

Harrison M, Campos JC, Masci P.  2015.  Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering. 11:95-111. Abstractharros.pdf

The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking systematically a set of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting. The devices differ as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety, these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.

Campos JC, Doherty G, Harrison M.  2014.  Analysing interactive devices based on information resource constraints. International Journal of Human-Computer Studies. 72(3):284-297. Abstract1-s2.0-s1071581913001407-main.pdf

Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.

Gomes T, Abade T, Campos JC, Harrison M, Silva JL.  2014.  A Virtual Environment based Serious Game to Support Health Education. EAI Endorsed Transactions on Ambient Systems. 14(3):e5. Abstractamsys.1.3.e5.pdf

APEX was developed as a framework for ubiquitous computing (ubicomp) prototyping through virtual environments. In this paper the framework is used as a platform for developing a serious game designed to instruct and to inform. The paper describes the Asthma game, a game aimed at raising awareness among children of asthma triggers in the home. It is designed to stimulate a healthier life-style for those with asthma and respiratory problems. The game was developed as the gamification of a checklist for the home environment of asthma patients.

Silva JL, Campos JC, Harrison M.  2014.  Prototyping and Analysing Ubiquitous Computing Environments using Multiple Layers. International Journal of Human-Computer Studies. 72(5):488-506. Abstractijhcs-silvach14-preprint.pdf

If ubiquitous computing (ubicomp) is to enhance physical environments then early and accurate assessment of alternative solutions will be necessary to avoid costly deployment of systems that fail to meet requirements. This paper presents APEX, a prototyping framework that combines a 3D Application Server with a behaviour modeling tool. The contribution of this framework is that it allows exhaustive analysis of the behaviour models that drive the prototype while at the same time enabling immersive exploration of a virtual environment simulating the proposed system. The development of prototypes is supported through three layers: a simulation layer (using OpenSimulator); a modelling layer (using CPN Tools) and a physical layer (using external devices and real users). APEX allows movement between these layers to analyse different features, from user experience to user behaviour. The multi layer approach makes it possible to express user behaviour in the modelling layer, provides a way to reduce the number of real users needed by adding simulated avatars, and supports user testing of hybrids of virtual and real components as well as exhaustive analysis. This paper demonstrates the approach by means of an example, placing particular emphasis on the simulation of virtual environments, low cost prototyping and the formal analysis capabilities.

Harrison M, Campos JC, Masci P.  2013.  Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering. 2(11):95-111. Abstractharrisoncm15-authorsversion.pdf

The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking a battery of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting but differ in a number of respects as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.

Silva CC, Mendonça C, Mouta S, Silva R, Campos JC, Santos J.  2013.  Depth cues and perceived audiovisual synchrony of biological motion. PLOS One. 8(1) Abstractjournal.pone_.0080096.pdf


Due to their different propagation times, visual and auditory signals from external events arrive at the human sensory receptors with a disparate delay. This delay consistently varies with distance, but, despite such variability, most events are perceived as synchronic. There is, however, contradictory data and claims regarding the existence of compensatory mechanisms for distance in simultaneity judgments.

Principal Findings

In this paper we have used familiar audiovisual events – a visual walker and footstep sounds – and manipulated the number of depth cues. In a simultaneity judgment task we presented a large range of stimulus onset asynchronies corresponding to distances of up to 35 meters. We found an effect of distance over the simultaneity estimates, with greater distances requiring larger stimulus onset asynchronies, and vision always leading. This effect was stronger when both visual and auditory cues were present but was interestingly not found when depth cues were impoverished.


These findings reveal that there should be an internal mechanism to compensate for audiovisual delays, which critically depends on the depth information available.

Campos JC, Machado J.  2013.  A Specification Patterns System for Discrete Event Systems' Analysis. International Journal of Advanced Robotic Systems. 10:315. Abstract45610.pdf

As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express properties of a system's behavior is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skillful process. Errors in this step of the process can create serious problems since a false sense of safety is gained with the analysis. However, when compared to the effort put into developing and applying modeling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements.

Freire L, Arezes P, Campos JC.  2012.  A literature review about usability evaluation methods for e-learning platforms. Work: A Journal of Prevention, Assessment and Rehabilitation. 41:1038-1044. Abstractfulltext.pdf

The usability analysis of information systems has been the target of several research studies over the past thirty years. These studies have highlighted a great diversity of points of view, including researchers from different scientific areas such as Ergonomics, Computer Science, Design and Education. Within the domain of information ergonomics, the study of tools and methods used for usability evaluation dedicated to E-learning presents evidence that there is a continuous and dynamic evolution of E-learning systems, in many different contexts -academics and corporative. These systems, also known as LMS (Learning Management Systems), can be classified according to their educational goals and their technological features. However, in these systems the usability issues are related with the relationship/interactions between user and system in the user’s context. This review is a synthesis of research project about Information Ergonomics and embraces three dimensions, namely the methods, models and frameworks that have been applied to evaluate LMS. The study also includes the main usability criteria and heuristics used. The obtained results show a notorious change in the paradigms of usability, with which it will be possible to discuss about the studies carried out by different researchers that were focused on usability ergonomic principles aimed at E-learning.

Campos JC, Harrison M.  2011.  Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST. 45 Abstract641-1972-1-pb.pdf

This paper is concerned with the scaleable and systematic analysis of interactive systems. The motivating problem is the procurement of medical devices. In such situations several different manufacturers offer solutions that support a particular clinical activity. Apart from cost, which is a dominating factor, the variations between devices are relatively subtle and the consequences of particular design features are not clear from manufacturers' manuals, demonstrations or trial uses. De- spite their subtlety these differences can be important to the safety and usability of the device. The paper argues that formal analysis of the range of offered devices can provide a systematic means of comparison. The paper also explores barriers to the use of such techniques, demonstrating how layers of specification may be used to make it possible to reuse common specification. Infusion pumps provide a motivating example. A specific model is described and analysed and comparison between competitive devices is discussed rather than dealt with in detail.

Machado J, Seabra E, Campos JC, Soares F, Le C.  2011.  Safe Controllers Design for Industrial Automation Systems. Computers & Industrial Engineering. 60(4):635-653. Abstractcaie-s-09-00536-paracctc.pdf

The design of safe industrial controllers is one of the most important domains related with Automation Systems research. For this purpose, there are used some important synthesis and analysis techniques. Among the analysis techniques two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. For the successful application of these mentioned techniques the plant modelling is crucial, so the understanding and modelling of the plant behaviour is essential for obtaining safe industrial systems controllers. A two step approach is presented: first, the use of Simulation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper makes it possible to deal with real industrial systems, and obtain safe controllers for hybrid plants. Modelica modelling language and Dymola simulation environment is used for Simulation purposes and Timed Automata formalism and UPPAAL real-time model-checker are used for Formal Verification purposes.

Silva JC, Campos JC, Saraiva JA.  2010.  GUI Inspection from Source Code Analysis. Electronic Communications of the EASST. 33 Abstract459-1337-1-pb.pdf

Graphical user interfaces (GUIs) are critical components of todays software. Given their increased relevance, correctness and usability of GUIs are becoming essential. This paper describes the latest results in the development of our tool to reverse engineer the GUI layer of interactive computing systems. We use static analysis techniques to generate models of the user interface behaviour from source code. Models help in graphical user interface inspection by allowing designers to concentrate on its more important aspects. One particularly type of model that the tool is able to generate is state machines. The paper shows how graph theory can be useful when applied to these models. A number of metrics and algorithms are used in the analysis of aspects of the user interface's quality. The ultimate goal of the tool is to enable analysis of interactive system through GUIs source code inspection.

Harrison M, Campos JC.  2008.  Analysing Human Aspects of Safety-Critical Software. ERCIM News. 75:18. Abstracten75-p18.pdf

In focusing on human system interactions, the challenge for software engineers is to build systems that allow users to carry out activities and achieve objectives effectively and safely. A well-designed system should also provide a better experience of use, reducing stress and frustration. Many methods aim to help designers to produce systems that have these characteristics. Our research is concerned with the use of formal techniques to help construct such interactive systems.

Silva JL, Campos JC, Paiva A.  2008.  Model-based user interface testing with Spec Explorer and ConcurTaskTrees. Electronic Notes in Theoretical Computer Science. 208:77-93. Abstract1-s2.0-s1571066108002132-main.pdf

Analytic usability analysis methods have been proposed as an alternative to user testing in early phases of development due to the cost of the latter approach. By working with models of the systems, analytic models are not capable of identifying implementation related problems that might have an impact on usability. Model-based testing enables the testing of an implemented software artefact against a model of what it should be (the oracle). In the case of model-based user interface testing, the models should be expressed at an adequate level of abstraction, adequately modelling the interaction process. This paper describes an effort to develop tool support enabling the use of task models as oracles for model-based testing of user interfaces.

Harrison M, Kray C, Campos JC.  2008.  Exploring an option space to engineer a ubiquitous computing system. Electronic Notes in Theoretical Computer Science. 208:41-55. Abstract1-s2.0-s1571066108002119-main.pdf

Engineering natural and appropriate interactive behaviour in ubiquitous computing systems presents new challenges to their developers. This paper explores formal models of interactive behaviour in ubiquitous systems. Of particular interest is the way that these models may help engineers to visualise the consequences of different designs. Design options based on a dynamic signage system (GAUDI) are explored using different instances of a generic model of the system.

Barbosa LS, Campos JC.  2007.  Towards a coordination model for interactive systems. Electronic Notes in Theorectical Computer Science. :73-88. Abstractbbc06_lsb.pdf

When modelling complex interactive systems, traditional interactor-based approaches suffer from lack of expressiveness regarding the composition of the different interactors present in the user interface model into a coherent system. In this paper we investigate an alternative approach to the composition of interactors for the specification of complex interactive systems which is based on the coordination paradigm. We layout the fundations for the work and present an illustrative example. Lines for future work are identified.

Mano A, Campos JC.  2006.  Usabilidade em interfaces para crianças. Jornal de Circunstâncias Cognitivas. Abstractjcc_v2.pdf

O estudo da interacção entre crianças e computadores tem recebido atenção crescente nos últimos anos (ver, por exemplo, a série de conferências em Interaction Design and Children). A utilização de meios informáticos, quer para actividades educativas, quer para actividades de lazer (bem como a sua integração), tem um potencial genericamente reconhecido. No entanto, é necessário estudar de que forma as crianças interpretam e interagem com as interfaces se pretendemos desenvolver sistemas bem sucedidos.
O objectivo do estudo apresentado nesta comunicação consistiu exactamente em estudar o modo como crianças entre os 5 e os 7 anos de idade interagem com computadores. Tal como mencionado, existe já investigação nesta área, e alguns conjuntos de guidelines de desenho estão já publicados (por exemplo, Gilutz e Nielsen, 2002). A diferença entre o presente estudo e outras publicações reside na forma como os dados serão obtidos e nos próprios objectivos do estudo. A principal meta do método utilizado não é descobrir o que as crianças podem ou não fazer numa interface, mas sim os motivos pelos quais elas conseguem ou não utilizá-la.

Campos JC, Harrison M.  2001.  Model checking interactor specifications. Automated Software Engineering. 8:275-310. Abstract

Recent accounts of accidents draw attention to “automation surprises” that arise in safety critical systems. An automation surprise can occur when a system behaves differently from the expectations of the operator. Interface mode changes are one class of such surprises that have significant impact on the safety of a dynamic interactive system. They may take place i>implicitly as a result of other system action. Formal specifications of interactive systems provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an i>interactor based specification has as a partial model of an interactive system so that mode consequences can be checked early in the design process. We show how interactor specifications can be translated into the SMV model checker input language and how we can use such specifications in conjunction with the model checker to analyse potential for mode confusion in a realistic case. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems. This verification process can be useful in raising questions that have to be addressed in a broader context of analysis.

Doherty G, Campos JC, Harrison M.  2000.  Representational Reasoning and Verification. Formal Aspects of Computing. 12(4):260-277. Abstractdohertych00.pdf

Formal approaches to the design of interactive systems rely on reasoning about properties of the system at a very high level of abstraction. Specifications to support such an approach typically provide little scope for reasoning about presentations and the representation of information in the presentation. In contrast, psychological theories such as distributed cognition place a strong emphasis on the role of representations, and their perception by the user, in the cognitive process. However, the post-hoc techniques for the observation and analysis of existing systems which have developed out of the theory do not help us in addressing such issues at the design stage. Mn this paper we show how a formalisation can be used to investigate the representational aspects of an interface. Our goal is to provide a framework to help identify and resolve potential problems with the representation of information, and to support understanding of representational issues in design. We present a model for linking properties at the abstract and perceptual levels, and illustrate its use in a case study of a ight deck instrument. There is a widespread consensus that proper tool support is a prerequisite for the adoption of formal techniques, but the use of such tools can have a profound effect on the process itself. In order to explore this issue, we apply a higher-order logic theorem prover to the analysis.