Guerreiro N, Mendes S, Pinheiro V, Campos JC.  2008.  AniMAL - a user interface prototyper and animator for MAL interactor models. Interac - International Conference on Human-Computer Interaction. :93-102. Abstract08gmpc-int08-versaopub.pdf

Engineering correct software is one of the grand challenges of computer science. Practical design and verification methodologies to ensure correct software can have a substantial impact on how programs are built by the industry. As human-machine systems become more functional, they also become more complex. Consequently, the interactions between the machine and its users becomes less predictable and more difficult to analyse. Using Model Checking it is possible to automatically analyse the behaviour of a modelled system. Hence, different authors have investigated the applicability of model checking to the analysis of human-machine interactions. The IVY workbench is a tool that supports system design and verification, by providing a model checking based integrated modelling and analysis environment. The tool is based around a plugin architecture, and although it features a verification results' analyser, it thus far lacked the ability to visually expose the sequence of events that lead to a system failure on a system's prototype. We propose the AniMAL plugin as an extension to the IVY workbench, providing automatic user interface prototyping and verification results' animation, while allowing thorough customisation.

Borges M, Campos JC, Ribeiro AN.  2008.  Framework de distribuição assíncrona de aplicações móveis situadas. Interac - International Conference on Human-Computer Interaction. :181-186. Abstractshort_paper_mborges_cameraready.pdf

Ao contrário das aplicações criadas para os computadores de secretária, as aplicações móveis podem tirar partido do facto de acompanharem o dispositivo em que estão a correr para diferentes locais. Estas localizações geográficas são um factor que permite que estas possam reagir e ajustar-se a realidades distintas. O trabalho apresentado neste artigo pretende ser um passo no sentido de aproximar as aplicações aos sítios físicos onde estas correm. É também uma aproximação ao problema da variabilidade dos dispositivos. Consiste numa framework para distribuição de aplicações que vão correr num gestor de aplicações pré- instalado em dispositivos móveis. Este gestor é responsável por actuar sobre a aplicação sempre que determinadas condições reais sejam atingidas. É também responsável por gerir o descarregamento das aplicações a partir das infraestruturas que as disponibilizam. Numa perspectiva qualitativa, e com base numa aplicação de teste desenvolvida, a framework revela-se adequada a distribuição de aplicações em ambientes móveis.

Campos JC, Machado J, Seabra E.  2008.  Property Patterns for the Formal Verification of Automated Production Systems. Proceedings of the 17th IFAC World Congress. :5107-5112. Abstract4192.pdf

In recent years, several approaches to the analysis of automation systems dependability through the application of formal verification techniques have been proposed. Much of the research has been concerned with the modelling languages used, and how best to express the automation systems, so that automated veri cation might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need veri cation. This is however a crucial aspect of the veri cation process. Writing appropriate properties, in a logic suitable for veri cation, is a skilful process, and indeed there have been reports of properties being wrongly expressed. In this paper we put forward a tool and a collection of property patterns that aim at providing help in this area.

Campos JC, Harrison M.  2008.  Systematic analysis of control panel interfaces using formal tools. 15th International Workshop on the Design, Verification and Specification of Interactive Systems - DSV-IS. :72-85. Abstract2012-dsvis08-ch.pdf

The paper explores the role that formal modeling may play in aiding the visualization and implementation of usability requirements of a control panel. We propose that this form of analysis should become a systematic and routine aspect of the development of such interfaces. We use a notation for describing the interface that is convenient to use by software engineers, and describe a set of tools designed to make the process systematic and exhaustive.

Doherty G, Campos JC, Harrison M.  2008.  Resources for Situated Actions. 15th International Workshop on the Design, Verification and Specification of Interactive Systems (DSV-IS 2008). Abstractdsvis08-preprint.pdf

In recent years, advances in software tools have made it easier to analyze interactive system specifications, and the range of their possible behaviors. However, the effort involved in producing the specifications of the system is still substantial, and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly, to facilitate a resource-based analysis of user activity, allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.

Machado J, Seabra E, Campos JC, Soares F, Leão C, Silva JF.  2007.  Simulation and Formal Verification of Industrial Systems Controllers. 19th International Congress of Mechanical Engineering - COBEM. Abstractpublicacao_-_ssm3_iii_09_-_publicado_em_2008.pdf

Actually, the safety control is one of the most important aspects studied by the international researchers, in the field of
design and development of automated production systems due to social (avoid work accidents, ...), economics (machine stop time
reduction, increase of productivity,...) and technological aspects (less risks of damage of the components,...). Some researchers of
the Engineering School of University of Minho are also studying these aspects of safety control, using simulation and modelchecking
techniques in the development of Programmable Logic Controllers (PLC) programs.
The techniques currently used for the guarantee of automated production systems control safety are the Simulation and the Formal
Verification. If the Simulation is faster to execute, has the limitation of considering only some system behavior evolution scenarios.
Using Formal Verification it exists the advantage of testing all the possible system behavior evolution scenarios but, sometimes, it
exists the limitation of the time necessary for the attainment of formal verification results. In this paper it is shown, as it is possible,
and desirable, to conciliate these two techniques in the analysis of PLC programs. With the simultaneous use of these two
techniques, the developed PLC programs are more robust and not subject to errors. It is desirable the use of simulation before using
formal verification in the analysis of a system control program because with the simulation of some possible system behaviors it is
possible to eliminate a set of program errors in reduced intervals of time and that would not happen if these errors were detected
only through the use of formal verification techniques. Conciliating these two techniques it can be substantially reduced the time
necessary for the attainment of results through the use of the formal verification technique.
For the analysis of a system control program for simulation and formal verification it is used the Dymola for the Simulation
(through the creation of system models with Modelica language) and UPPAAL (through the creation of system models with timed

Machado J, Seabra E, Soares F, Campos JC.  2007.  A New Plant Modelling Approach For Formal Verification Purposes. 11th IFAC/IFORS/IMACS/IFIP Symposium on Large Scale Systems - Theory and Applications (LSS 2007). Abstractifac-lss-2007011-01jul-0167mach.pdf

This paper presents a new approach in plant modeling for the formal verification of real time systems. A system composed by two tanks is used, where all its components are modeled by simple modules and all the interdependences of the system?s modular models are presented. As innovating parameters in the plant modeling, having as purpose its use on formal verification tasks, the plant is modeled using Dymola software and Modelica programming language. The results obtained in simulation are used to define the plant models that are used for the formal verification tasks, using the model-checker UPPAAL. The paper presents, in a more detailed way, the part of this work that is related to formal verification, being pointing out the used plant modeling approach.

Pinto H, José R, Campos JC.  2007.  An Interaction Model and Infrastructure for Localized Activities in Pervasive Computing Environments. IEEE International Conference on Pervasive Services 2007 (ICPS'07). :232-241. Abstractpinto-jose-campos-final.pdf

This paper presents an interaction model for pervasive computing environments supporting localized activities, i.e., activities strongly associated to a specific physical environment. We are particularly interested in activities performed by occasional visitors to public spaces. This interaction model is characterized by an activity-centered approach to pervasive computing and is defined in a conceptual model inspired by Activity Theory. ActivitySpot, a software infrastructure implementing this conceptual model, is also presented. User interaction in ActivitySpot is based on simple, everyday pervasive computing devices, which facilitates usage learning and allows for a wide user population. ActivitySpot has supported the deployment of several pervasive computing solutions for localized activities. Our conceptual model has been evaluated by user studies run at different public spaces and global results demonstrate the model’s suitability to the targeted type of scenario.

Ribeiro AN, Campos JC, Martins F.  2007.  Integrating HCI into a UML based Software Engineering course. Proceedings HCI Educators 2007. :48-57. Abstracthcied_fv.pdf

Software Engineering (SE) and HCI (Human Computer Interaction) are not the same age, do not have the same history, background or foundations, and did never share design principles and design models. The separation principle, by encouraging separate concerns and techniques to design the interactive and the computational layers of a software system - despite being absolutely correct from several SE crucial design principles, like modularity, separation of concerns, encapsulation, context independence and so on -, has sometimes been misjudged and mistakenly used. Therefore, instead of bridging the gap between the two separate de- signs, it helped widening that gap. However, the principle does not mention and does not impose any restrictions on how the integration should be done. In the context of a software engineering course the authors have been involved with for some years, the need has arisen to provide students with HCI skills. Several attempts at integrating HCI into software engineering can be found in the literature. However, none seemed amenable to application in the context of the course, basically because none of them could be taught and learnt in such a way (methodology) that could easily be blent into the software engineering design process. We present a methodological process that we have been teaching that aims at shortening the gap that software engineering students face when trying to adapt SE techniques to the interactive layer.

Chatty S, Campos JC, Gonzalez M, Lepreux S, Nilsson E, Penichet V, den Bergh SV.  2007.  Processes: Working group report. Interactive Systems: Design, Specification and Verification - Interactive Systems: Design, Specification and Verification - DSV-IS. 4323:262-264. Abstractwgreport-chatty.pdf

It has often been suggested that model-driven development of user interfaces amounted to producing models of user interfaces then using automatic code generation to obtain the final result. However, this may be seen as an extreme interpretation of the model-driven approach. There are examples where that approach is successful, including mobile computing and database management systems. But in many cases automatic generation may be either impossible or may limit the quality of the final interface.

Silva JC, Campos JC, Saraiva JA.  2007.  Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications. Design, Specification and Verification: Interactive Systems - DSV-IS. 4323:137-150. Abstractjcsilva06.pdf

Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI’s code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper describes our approach to reverse engineer an abstract model of a user interface directly from the GUI’s legacy code. We also present results from a case study. These results are encouraging and give evidence that the goal of reverse engineering user interfaces can be met with more work on this technique.

Campos JC, Doherty G.  2006.  Supporting resource-based analysis of task information needs. Interactive Systems: Design, Specification and Verification - DSV-IS. 3941:188-200. Abstractcamposdoherty-final.pdf

We investigate here an approach to modelling the dynamic information requirements of a user performing a number of tasks, addressing both the provision and representation of information, viewing the information as being distributed across a set of resources. From knowledge of available resources at the user interface, and task information needs we can identify whether the system provides the user with adequate support for task execution. We look at how we can use tools to help reason about these issues, and illustrate their use through an example.We also consider a full range of analyses suggested using this approach which could potentially be supported by automated reasoning systems.

Campos JC, Ribeiro AN.  2006.  UML no Desenvolvimento de Sistemas Interactivos. Interação 2006 - Actas da 2ª Conferência Nacional em Interacão Pessoa-Máquina. :77-80. Abstract31_anr.pdf

Os processos típicos de análise e modelação de sistemas numa perspectiva de engenharia de software atribuem pouca importância à modelação da camada interactiva. O Unified Process e a linguagem que o suporta (UML) não são excepção. Este artigo propõe uma abordagem, que procura integrar a modelação da camada interactiva no processo de modelação típico baseado em UML, explorando as potencialidades fornecidas pela linguagem.

Mano A, Campos JC.  2006.  Cognitive walkthroughs in the evaluation of user interfaces for children. Interação 2006 - Actas da 2a. Conferência Nacional em Interação Pessoa-Máquina. :195-198. Abstract7-prov_jose_campos_1.pdf

This paper describes a case-study, dealing with the application of the cognitive walkthrough as a meth od of evaluating an interface built for children. We perf ormed the walkthrough and tested the interface with children aged between 5 and 7 years old. Given our goals and the scope of this study, the cognitive walkthrough proved as a reliable source of indications about usability problems on an interface aimed at children.

Rodrigues S, Campos JC, Ribeiro AN.  2006.  Adaptação nativa de interfaces com o utilizador em dispositivos móveis. CSMU 2006 - Conference on Mobile and Ubiquitous Systems. :171-174. Abstractpapercsmu_anr.pdf

Neste artigo apresentamos o trabalho que tem vindo a decorrer no desenvolvimento de uma framework que permita a adaptação de interfaces com o utilizador directamente no ambiente nativo dos dispositivos, fornecendo assim ao utilizador interfaces de aplicações adequadas ao dispositivo, e ao estilo de interacção a que o utilizador está habituado.