Publications

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.

Gomes T, Abade T, Silva JL, Campos JC.  2013.  Desenvolvimento de Jogos Educativos na plataforma APEX: O Jogo da Asma. Atas da Conferência Interação. :90-97. Abstractgomesasc2013-interacao.pdf

A plataforma APEX foi desenvolvida para a prototipagem de ambientes de computação ubíqua. Neste artigo exploramos a sua aplicabilidade ao desenvolvimento de jogos sérios, ou seja, jogos que para além de uma componente lúdica, possuem uma componente instrutiva e formativa. Em concreto, descrevemos o Jogo da Asma. Um jogo que pretende chamar a atenção das crianças para os factores causadores de ataques de asma, bem como transmitir conhecimento sobre como os evitar. Para além de descrever o jogo, descrevem-se os resultados de um estudo em que se procurou avaliar quer a viabilidade da utilização da plataforma na criação de jogos sérios, quer a usabilidade do próprio jogo.

Abade T, Gomes T, Silva JL, Campos JC.  2013.  Avaliação de Ambientes Ubíquos na Plataforma APEX. Atas da Conferência Interação 2013. :177-178. Abstractabadegsc2013-interacao.pdf

Este artigo descreve a avaliação de um ambiente ubíquo utilizando a APEX, uma plataforma de prototipagem rápida de ambientes ubíquos que permite que os utilizadores naveguem num mundo virtual, podendo experimentar muitas das funcionalidades da solução e do design proposto.

Cruz P, Campos JC.  2013.  Ambiente de geração, mutação e execução de casos de teste para aplicações Web. Atas da Conferência Interação 2013. :45-52. Abstractcruzc2013-interacao.pdf

Cada vez mais as interfaces gráficas são um ponto-chave entre a comunicação dos utilizadores e o sistema. Para garantir que estas executam devidamente uma adequada fases de testes é essencial. No entanto, a execução de testes numa interface é um processo dispendioso e moroso, sendo estes tipicamente executados de forma manual. Neste artigo é explorada a automatização do processo de teste de interfaces para aplicações Web. Adopta-se uma abordagem de testes baseados em modelos. Os casos de teste são gerados recorrendo a modelos de tarefas e o comportamento da interface comparado com o que está prescrito no modelos de tarefas. Uma ferramenta que suporta a abordagem está em desenvolvimento.

Gomes T, Abade T, Harrison M, Silva JL, Campos JC.  2013.  Developing Serious Games With The APEX Framework. Proceedings of the Workshop on Ubiquitous games and gamification for promoting behavior change and wellbeing. :37-40. Abstractdeveloping-games-apex-final.pdf

APEX was developed as a framework for the prototyping of ubiquitous computing (ubicomp) environments. In this paper we explore its role as a platform for developing serious games. In particular we describe the Asthma game, a game aimed at raising awareness of asthma triggers among children, thus stimulating a healthier life-style in what concerns asthma and respiratory problems.

Silva CE, Campos JC.  2013.  Combining Static and Dynamic Analysis for the Reverse Engineering of Web Applications. Proceedings of the 5th Symposium on Engineering Interactive Computing Systems - EICS. :107-112. Abstracteics13.pdf

Software has become so complex that it is increasingly hard to have a complete understanding of how a particular system will behave. Web applications, their user interfaces in particular, are built with a wide variety of technologies making them particularly hard to debug and maintain. Reverse engineering techniques, either through static analysis of the code or dynamic analysis of the running application, can be used to help gain this understanding. Each type of technique has its limitations. With static analysis it is difficult to have good coverage of highly dynamic applications, while dynamic analysis faces problems with guaranteeing that generated models fully capture the behavior of the system. This paper proposes a new hybrid approach for the reverse engineering of web applications' user interfaces. The approach combines dynamic analyzes of the application at runtime, with static analyzes of the source code of the event handlers found during interaction. Information derived from the source code is both directly added to the generated models, and used to guide the dynamic analysis.

Silva JC, Silva JL, Campos JC, Saraiva JA.  2013.  Uma Abordagem para a Geração de Casos de Teste Baseada em Modelos. Sistemas e Tecnologias de Informação. 2:142-146. Abstractid-265-jcsilva.pdf

The analytical methods based on evaluation models of interactive systems were proposed as an alternative to user testing in the last stages of the software development due to its costs. However, the use of isolated behavioral models of the system limits the results of the analytical methods. An example of these limitations relates to the fact that they are unable to identify implementation issues that will impact on usability. With the introduction of model-based testing we are enable to test if the implemented software meets the specified model. This paper presents an model-based approach for test cases generation from the static analysis of source code.

Moreira S, José R, Campos JC.  2013.  An empirical study on immersive prototyping dimensions. Human-Computer Interaction: Human-Centred Design Approaches, Methods, Tools and Environments - HCI. 8004:421-430. Abstractmoreirajc13-hcii2013.pdf

Many aspects of the human experience of ubiquitous computing in built environments must be explored in the context of the target environment. However, delaying evaluation until a version of the system can be deployed can make redesign too costly. Prototypes have the potential to solve this problem by enabling evaluation before actual deployment. This paper presents a study of the design space of immersive prototyping for ubiquitous computing. It provides a framework to guide the alignment between speci c evaluation goals and speci c prototype properties. The goal is to understand the potential added-value of 3D simulation as a prototyping tool in the development process of ubiquitous computing environments.

Machado J, Campos JC.  2013.  Development of Dependable Controllers in the Context of Machines Design. Proceedings of International Conference of Machine Design Departments. Abstracticmd_paper

Abstract In the domain of machines' design, one of the most important issues to solve is related with the controller's design, mainly, guaranteeing that the machine will behave as expected. In order to achieve a dependable controller, some steps can be considered, such as the formalization of its specification - before being translated to the program that will be inserted in the controller device - and the respective analysis and verification. Nowadays, some formal analysis techniques, such as formal verification, are used to achieve this purpose. The dependability of a controller, however, is impacted by its execution context. This paper proposes an approach for the formal verification of the specification of mechatronic system's controllers, which considers, on the formal verification tasks, the behavior of the plant and the behavior of the Human Machine Interface of the Mechatronic system. Some conclusions are extrapolated for other systems of the same kind.

Oliveira L, Ribeiro AN, Campos JC.  2013.  The Mobile Context Framework: providing context to mobile applications. The 27th International British Computer Society Human Computer Interaction Conference: The Internet of things - HCI. 8028 Abstractoliveirarc13-hcii2013.pdf

The spread of mobile devices in modern societies has forced the industry to create software paradigms to meet the new challenges it faces. Some of these challenges are the huge heterogeneity of devices or the quick changes of users’ context. In this scenario, context becomes a key element, enabling mobile applications to be user centric and adapt to user requirements. The Mobile Context Framework, proposed in this paper, is a contribution to solve some of these challenges. Using Web servers running on the devices, context data can be provided to web applications. Besides the framework’s architecture, a prototype is presented as proof of concept of the platform’s potential.

Campos JC, Abreu R.  2013.  Encoding Test Requirements as Constraints for Test Suite Minimization. Tenth International Conference on Information Technology: New Generations - ITNG. :317–322. Abstractjosecampos-itng-2013.pdf

Software (regression) testing is performed not only to detect errors as early as possible but also to guarantee that changes did not affect the system negatively. As test suites tend to grow over time, e.g., new test cases are added to test new features, (re-)executing the entire suite becomes prohibitive. We propose an approach, RZOLTAR, addressing this issue: it encodes the relation between a test case and its testing requirements (code statements in this paper) in a so-called coverage matrix; maps this matrix into a set of constraints; and computes a set of optimal solutions (main taining the same coverage as the original suite) by leveraging a fast constraint solver. We show that RZOLTAR efficiently (0.68 seconds on average) finds a collection of test suites that significantly reduce the size of the original suite (61.12%), while greedy only finds one solution with a reduction of 56.58% in 6.92 seconds on average.

Machado P, Campos JC, Abreu R.  2013.  MZoltar: automatic debugging of Android applications. Proceedings of the 2013 International Workshop on Software Development Lifecycle for Mobile - DeMobile. :9–16. Abstractpedromachado-demobile-2013.pdf

Automated diagnosis of errors and/or failures detected during software testing can greatly improve the eciency of the debugging process, and thus help to make applications more reliable. In this paper, we propose an approach, dubbed MZoltar, o ering dynamic analysis (namely, spectrum- based fault localization) of mobile apps that produces a diagnostic report to help identifying potential defects quickly. The approach also o ers a graphical representation of the diagnostic report, making it easier to understand. Our experimental results show that the approach requires low runtime overhead (5.75% on average), while the tester needs to inspect 5 components (statements in this paper) on average to a nd the fault.

Campos JC, Abreu R, Fraser G, d'Amorim M.  2013.  Entropy-based test generation for improved fault localization. IEEE/ACM 28th International Conference on Automated Software Engineering - ASE). :257–267. Abstractcampos-etal-ase2013.pdf

Spectrum-based Bayesian reasoning can effectively rank candidate fault locations based on passing/failing test cases, but the diagnostic quality highly depends on the size and diversity of the underlying test suite. As test suites in practice often do not exhibit the necessary properties, we present a technique to extend existing test suites with new test cases that optimize the diagnostic quality. We apply probability theory concepts to guide test case generation using entropy, such that the amount of uncertainty in the diagnostic ranking is minimized. Our ENTBUG prototype extends the search-based test generation tool EVOSUITE to use entropy in the fitness function of its underlying genetic algorithm, and we applied it to seven real faults. Empirical results show that our approach reduces the entropy of the diagnostic ranking by 49% on average (compared to using the original test suite), leading to a 91% average reduction of diagnosis candidates needed to inspect to find the true faulty one.

Gouveia C, Campos JC, Abreu R.  2013.  Using HTML5 visualizations in software fault localization. First IEEE Working Conference on Software Visualization - VISSOFT. :1–10. Abstractcarlosgouveia-vissoft-2013.pdf

Testing and debugging is the most expensive, error-prone phase in the software development life cycle. Automated software fault localization can drastically improve the efficiency of this phase, thus improving the overall quality of the software. Amongst the most well-known techniques, due to its efficiency and effectiveness, is spectrum-based fault localization. In this paper, we propose three dynamic graphical forms using HTML5 to display the diagnostic reports yielded by spectrum-based fault localization. The visualizations proposed, namely Sunburst, Vertical Partition, and Bubble Hierarchy, have been implemented within the GZOLTAR toolset, replacing previous and less-intuitive OpenGL-based visualizations. The GZOLTAR toolset is a plug-and-play plugin for the Eclipse IDE to ease world-wide adoption. Finally, we performed an user study with GZOLTAR and confirmed that the visualizations help to drastically reduce the time needed in debugging (e.g., all participants using the visualizations were able to pinpoint the fault, whereas of those using traditional methods only 35% found the fault). The group that used the visualizations took on average 9 minutes and 17 seconds less than the group that did not use them.

Harrison M, Masci P, Campos JC, Curzon P.  2013.  Automated theorem proving for the systematic analysis of interactive systems. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems. Abstractharrisonmcc.pdf

This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.