Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About
Download Photo HD

About

I am an assistant professor at the Department of Informatics of the University of Minho and a senior researcher at HASLab - INESC TEC. I mainly work on the application of formal software engineering techniques and tools to the modelling and analysis of interactive system. 

Current and recent funded research includes: formal modelling and analysis of interactive systems (with a particular focus on medical devices); model-based testing of user interfaces; prototyping of ambience intelligence systems using virtual reality simulations; and the reverse engineering of the user interface layer of software systems.

I am a member of IFIP WG 2.7/13.4 on User Interface Engineering (currently chairing the group) and of the steering committee of EICS (the ACM SIGCHI Symposium on Engineering Interactive Computer Systems).

Interest
Topics
Details

Details

  • Name

    José Creissac Campos
  • Role

    Senior Researcher
  • Since

    01st November 2011
  • Nationality

    Portugal
  • Contacts

    +351253604440
    jose.c.campos@inesctec.pt
007
Publications

2020

Model-based testing of post-wimp interactions using object oriented petri-nets

Authors
Canny, A; Navarre, D; Campos, JC; Palanque, P;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Model-Based Testing (MBT) relies on models of a System Under Test (SUT) to derive test cases for said system. While Finite State Machine (FSM), workflow, etc. are widely used to derive test cases for WIMP applications (i.e. applications depending on 2D widgets such as menus and icons), these notations lack the expressive power to describe the interaction techniques and behaviors found in post-WIMP applications. In this paper, we aim at demonstrating that thanks to ICO, a formal notation for describing interactive systems, it is possible to generate test cases that go beyond the state of the art by addressing the MBT of advanced interaction techniques in post-WIMP applications. © Springer Nature Switzerland AG 2020.

2019

Formal techniques in the safety analysis of software components of a new dialysis machine

Authors
Harrison, MD; Freitas, L; Drinnan, M; Campos, JC; Masci, P; di Maria, C; Whitaker, M;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
The paper is concerned with the practical use of formal techniques to contribute to the risk analysis of a new neonatal dialysis machine. The described formal analysis focuses on the controller component of the software implementation. The controller drives the dialysis cycle and deals with error management. The logic was analysed using model checking techniques and the source code was analysed formally, checking type correctness conditions, use of pointers and shared memory. The analysis provided evidence of the verification of risk control measures relating to the software component. The productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and the analyst using the formal analysis tools, provided a basis for the development of rationale for the effectiveness of the evidence.

2019

Verification Templates for the Analysis of User Interface Software Design

Authors
Harrison, MD; Masci, P; Campos, JC;

Publication
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

Abstract
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.

2019

IVY 2: A model-based analysis tool

Authors
Couto, R; Campos, JC;

Publication
Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2019

Abstract
The IVY workbench is a model-based tool that supports the formal verification of interactive computing systems. It adopts a plugin-based architecture to support a flexible development model. Over the years the chosen architectural solution revealed a number of limitations, resulting both from technological deprecation of some of the adopted solutions and a better understanding of the verification process to support. This paper presents the redesign and implementation of the original plugin infrastructure, originating a new version of the tool: IVY 2. It describes the limitations of the original solutions and the new architecture, which resorts to the Java module system in order to solve them. © ACM 2019.

2019

IVY 2

Authors
Couto, R; Campos, JC;

Publication
Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems - EICS '19

Abstract

Supervised
thesis

2019

Using Predictive and Descriptive Cognitive Models for Evaluation of Interactive Computing Systems

Author
Carlos César Loureiro Silva

Institution
UM

2019

Gerador de protótipos de interfaces gráficas para IVY Workbench

Author
João Miguel Matela Aidos Manso de Araújo

Institution
UM

2018

Modern Front-End Web Development

Author
António Manuel Pereira do Anjo

Institution
UM

2018

Simulação de dispositivos médicos em Android

Author
André Miguel Bonjardim Pinto

Institution
UM

2018

Teste baseado em modelos de aplicações Android

Author
Pedro Miguel Braga do Vale

Institution
UM