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.

Calvary G, Nichols J, Campos JC, Nunes N, Campos P.  2017.  Welcome to the First Issue of PACMHCI EICS [Editorial]. Proc. ACM Hum.-Comput. Interact.. 1:1:1–1:2. Abstract


Campos JC, Doherty G, Harrison M.  2009.  Repository of models of interactive behaviour.
Sousa N, Campos JC.  2006.  IVY Trace Visualizer. Abstract17_yvy_jose_campos_1.pdf

No contexto do projecto IVY, tem vindo a ser desenvolvida uma ferramenta de modelação e análise de sistemas interactivos, tendo em vista a detecção de potenciais problemas de usabilidade no início do desenvolvimento de um qualquer sistema interactivo. Quando uma dada propriedade em análise não se verifica, a ferramenta procura indicar um contraxemplo: um comportamento do modelo que demonstre a falsidade da propriedade em questão. Estes contra-exemplos, no entanto, podem atingir tamanhos consideráveis, dependendo da complexidade do modelo, o que dificulta a sua análise. De forma a facilitar essa análise, a arquitectura da ferramenta IVY prevê um componente de suporte à análise. Este componente visa, através de representações visuais e de mecanismos de análise, facilitar a compreensão dos contra exemplos, de forma a tornar mais claro qual o problema que está a ser apontado e possíveis soluções para o mesmo. Este artigo apresenta o componente de análise da ferramenta IVY. São apresentadas a arquitectura do componente, as representações implementadas e os mecanismos de análise disponibilizados.

Sousa N, Campos JC.  2006.  Technical Manual for the Trace Visualiser.
Sousa N, Campos JC.  2006.  Um visualizador de traços de comportamento para a ferramenta IVY. Abstractivy-tr-5-03.pdf

This report describes the development of a component (Trace Visualiser) for a modular tool named IVY (Interactors VerYfier).