Sousa N, Campos JC.  2006.  User Manual for the Trace Visualiser.
Harrison M, Doherty G, Campos JC.  2005.  Is there a role for rigorous system analysis in experience centred design? Abstractmdhmauserev8.pdf

This chapter explores the role that formal modelling may play in aiding the visualization and implementation of usability, with a particular emphasis on experience requirements in an ambient and mobile system. Mechanisms for requirements elicitation and evaluation are discussed, as well as the role of scenarios and their limitations in capturing experience requirements. The chapter then discusses the role of formal modelling by revisiting an analysis based on an exploration of traditional usability requirements before moving on to consider requirements more appropriate to a built environment. The role of modelling within the development process is re-examined by looking at how models may incorporate knowledge relating to user experience, and how the results of the analysis of such models may be exploited by human factors and domain experts in their consideration of user experience issues.

Ridder A, Posadas F, Campos JC.  2005.  Technical Guide for the Visualiser Component.
Campos JC.  2004.  Interactors as Boundary Objects. Abstractcamposch01ws.pdf

Too often software engineers see the user interface as a last layer that must be placed on top of the functional (or business logic) layer in order (simply?) to enable users access to its functionality. This vision rests on the assumption that all the application’s logic is at the functional level, and is independent of the user interface. The user interface then is simply a information transmission layer between the user and the “application” (i.e., the functional layer).

Campos JC, Harrison M.  1999.  From Interactors to SMV: A Case Study in the Automated Analysis of Interactive Systems. Abstractycs-99-317.pdf

Recent accounts of accidents have drawn attention to problems that arise in safety critical systems through “automation surprises”. A particular class of such surprises, interface mode changes, may have significant impact on the safety of a dynamic interactive system and may take place implicitly as a result of other system action. Formal specifications of interactive systems may provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification may have as a partial model of an interactive system, so that mode consequences might 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, and, in this context, we show how the verification process can be useful by raising questions that have to be addressed in a broader context of analysis.

Campos JC.  1995.  GAMA-X - MIU Programmer's Manual. Abstractmiu_prog_man95.pdf

The GAMA-X system is a semi-automatic generator of assisted interfaces  . It aims at being an UIMS (User Interface Management System) for the Camila system  capable of providing an user interface that can be used at all levels of the application development cycle from the prototype to the nal implementation. The GAMA-X system is divided into two main modules the MGI (Interface Generation Module) and the MIU (User Interaction Module). The MGI generates an user interface specication or MIU specication from the computational layer specication The MIU creates an user interface based on the specication generated by the MGI. The MIU specications can be generated by the MGI or hand written from scratch In this manual we show with an example how to write the MIU specication.

Campos JC, Martins F.  1994.  Automatic Generation of User Interfaces at Prototype Level. Abstract

This report puts forward a software architecture aimed at providing tecnological support for User Interface design in the framework of a rigorous methodology for Interactive Systems development. Starting from the formal specification of the application layer, the methodology aims at the systematic development of the interactive system, with the main goal of creating high quality interfaces with a high degree of assistance to the user, error preventing features and contextual sensitivity. The proposed system, GAMA-X, offers an architecture for the systematic and semi-automatic development of this kind of interface, including tools that support the various steps of development. The architecture of the GAMA-X system is presented, with a special focus on the modules more closely related with the User Interface, as well as the description of a specification language for the Dialogue Controller. Some aspects about the communication between modules and about the presentation layer are also discussed.

Madeira F, Campos JC, Castro P, Martins F.  1990.  GAMA - Geração Automática de Modo Assistido.
Couto R, Ribeiro AN, Campos JC.  2017.  Pattern Based Software Development (PhD thesis). Approved, Very Goodcouto_phdthesis.pdf
Campos JC.  1999.  Automated Deduction and Usability Reasoning. Abstractycst-2000-09.pdf

Reasoning about the usability of a given interactive system's design is a difficult task. However it is one task that must be performed if downstream costs with extensive redesign are to be avoided. Traditional usability testing alone cannot avoid these costs since it too often is performed late in development life cycle. In recent years approaches have been put forward that attempt to reason about the usability of a design from early in development. Mainstream approaches are based on some kind of (more or less structured) inspection of a design by usability experts. This type of approach breaks down for systems with large and complex user interfaces, and again extensive testing is required. In an attempt to deal with these issues there have been attempts to apply software engineering reasoning tools to the development of interactive systems. The article reviews this work and puts forward some ideas for the future.

Campos JC.  1993.  GAMA- X - Geração Semi-Automática de Interfaces Sensíveis ao Contexto. Abstractmestrado.pdf

A separação dos sistemas interactivos em componente computacional e componente de diálogo, veio possibilitar o aparecimento de tecnologia, específica para a implementação de interfaces com o utilizador. No entanto, apesar da grande quantidade de tecnologia disponível, a construção de uma interface é ainda um processo difícil e demorado. Tal situação, deu origem ao estudo e desenvolvimento de metodologias que permitam especificar formalmente o diálogo humano-computador, tendo em vista um desenvolvimento mais rápido e seguro da referida camada. A interface de um sistema interactivo não deve ser apenas um meio de transmissão passivo entre o utilizador e a aplicação, mas um reflexo da aplicação, permitindo ao utilizador saber o estado actual da mesma facilitando-lhe, assim, o diálogo com ela. A separação demasiado rígida, proposta por muitos modelos, entre camada computacional e camada de diálogo não permite o desenvolvimento de interfaces deste tipo, uma vez que a informação semântica se encontra encapsulada na componente computacional. Com base nestas constatações, foi estudado e implementado um formalismo de especificação de diálogo - Guiões de Interacção - que permite a inclusão de condições semãnticas na especificação, possibilitando expressar claramente e diferenciar as componentes dinâmicas do diálogo, em particular “o diálogo sensível ao con da aplicação”. A utilização de uma notação a la CCS permite a especificação de diálogos concorrentes, tendo-se utilizado Petri Nets para lhes dar semântica e como modelo de implementação dos Guiões de Interacção. É ainda apresentada a arquitectura do sistema GAMA-X - um UIMS para a linguagem CAMILA baseado em Guiões de Interacção - e feita a implementação da componente de runtime do mesmo, provando, deste modo, a validade dos Guiões de Interacção enquanto formalismo para a especificação de diálogo.