José Creissac Campos

Recent Publications / Publicações Recentes

Accepted

abstracts on (turn off)

E. Moreira and J.C. Campos
On the role of generative AI in explaining model checking counterexamples. In L. Zaina and others, editors, Engineering Interactive Computer Systems, volume 15518 of Lecture Notes in Computer Science. Springer. (in press)

J. C. Campos and M. D. Harrison
Formal approaches for Interactive Systems. In J. Vanderdonckt, P. Palanque and M. Winckler, editors, Handbook of Human Computer Interaction. Springer.
 

2024

abstracts on (turn off)

E. Moreira and J.C. Campos (2024)
A language for explaining counterexamples. In 13th Symposium on Languages, Applications and Technologies (SLATE 2024), volume 120 of OpenAccess Series in Informatics (OASIcs), pages 11:1-11:14. Schloss Dagstuhl - LZI.
Model checkers can automatically verify a system's behavior against temporal logic properties. However, analyzing the counterexamples produced in case of failure is still a manual process that requires both technical and domain knowledge. However, this step is crucial to understand the flaws of the system being verified. This paper presents a language created to support the generation of natural language explanations of counterexamples produced by a model checker. The language supports querying the properties and counterexamples to generate the explanations. The paper explains the language components and how they can be used to produce explanations.
 

A. Cunha, N. Macedo, J.C. Campos, I. Margolis and E. Sousa (2024)
Assessing the impact of hints in learning formal specification. In International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET 2024), pages 145-155. ACM.
Background: Many programming environments include automated feedback in the form of hints to help novices learn programming autonomously. Some experimental studies investigated the impact of automated hints in the immediate performance and learning retention in that context. Automated feedback is also becoming a popular research topic in the context of formal specification languages, but so far no experimental studies have been conducted to assess the impact of hints while learning such languages. Objective: We aim to investigate the impact of different types of automated hints while learning a formal specification language, not only in terms of immediate performance and learning retention, but also in the emotional response of the students. Method: We conducted a simple one-factor randomised experiment in 2 sessions involving 85 undergraduate students majoring in CSE. In the 1st session students were divided in one control group and three experimental groups, each receiving a different type of hint while learning to specify simple requirements with the Alloy formal specification language. To assess the impact of hints on learning retention, in the 2nd session, 1 week later, all students had no hints while formalising requirements. Before and after each session the students answered a standard self-reporting emotional survey to assess their emotional response to the experiment. Results: Of the three types of hints we evaluated, only the ones that point to the precise location of an error had a positive impact on the immediate performance and none of them had significant impact in the learning retention. Hint availability also causes a significant impact on the emotional response, but no significant emotional impact exists once hints are no longer available (e.g. no significant deprivation effects were detected). Conclusion: Although none of the evaluated hints had an impact on learning retention, learning a formal specification language with an environment that provides hints with precise error locations seems to contribute to a better overall experience without apparent drawbacks. Further studies are needed to investigate if other kinds of hints, namely hints combined with some sort of self-explanation prompts, can have a positive impact in learning retention.
 

L.D. Spano, J.C. Campos, A. Dittmar and P. Forbrig (2024)
An Online Repository for Educational Resources in HCI-Engineering. In Design for Equality and Justice, volume 14535 of Lecture Notes in Computer Science, pages 183-200. Springer.
This paper leverages the outcomes of the first workshop on HCI Engineering Education to create an online repository where the community can share content relevant to HCI. The repository takes advantage of the functionalities of the Git file versioning system to support presenting and adding content. The paper describes the structure of the repository and the process for adding new content. In addition, we propose an adaptation of the framework for presenting teaching samples, supporting more flexibility in the application of educational material for different teaching objectives. The new presentation format starts with describing a design problem and emphasises the students' applied understanding of conceptual and theoretical knowledge. The presentation format is demonstrated and discussed by the example of an end-user design tool for mobile data collection.
 

E. Moreira and J.C. Campos (2024)
Explaining temporal logic model checking counterexamples through the use of structured Natural Language. In Engineering Interactive Computer Systems, volume 14517 of Lecture Notes in Computer Science, pages 1-19. Springer.
The use of model checking tools allows for the formal verification of properties over models of systems, improving their robustness. However, these tools are challenging to use, and their results require much work of interpretation to communicate to stakeholders. To address this issue, the IVY Workbench offers a plethora of options to make the process of creating and understanding the models, properties and results of the verification process more accessible, with a particular focus on interactive computing systems. Despite this, there is still a significant requirement of expertise to use the tool. To solve this, an approach to provide structured natural language explanations for the results of model checking-based tools is being developed, to be later incorporated into the IVY Workbench. This paper presents the current state of the approach's development, stating its objective and what results can already be achieved.
 

2023

abstracts on (turn off)

R. Braga da Costa and J.C. Campos (2023)
Prototyping with the IVY Workbench: Bridging Formal Methods and User-Centred Design. In Human-Computer Interaction - INTERACT 2023, volume 14143 of Lecture Notes in Computer Science, pages 504-513. Springer.
 

B. Teixeira and J.C. Campos (2023)
Towards Automated Load Testing Through the User Interface. In Human-Computer Interaction - INTERACT 2023, volume 14143 of Lecture Notes in Computer Science, pages 514-522. Springer.
 

P.A. Palanque and J.C. Campos (2023)
AMAN Case Study. In Rigorous State-Based Methods - ABZ 2023, volume 14010 of Lecture Notes in Computer Science, pages 265-283. Springer.
 

2022

abstracts on (turn off)

J. Martins, J.M. Fonseca, R. Costa, J.C. Campos, A. Cunha, N. Macedo and J.N. Oliveira (2022)
Verification of Railway Network Models with EVEREST. In MODELS '22, pages 345-355. ACM.
Models - at different levels of abstraction and pertaining to different engineering views - are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model - the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD) - in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions.
 

J.C. Campos and A.N. Ribeiro (2022)
Addressing Interactive Computing Systems' concerns in Software Engineering degrees. In Feel, Sense, Design - INTERACT 2021 IFIP TC 13 Workshops, volume 13198 of Lecture Notes in Computer Science, pages 248-256. Springer.
 

S. Caffieau, J.C. Campos, C. Martinie, L. Nigay, P. Palanque and L.D. Spano (2022)
Teaching HCI Engineering: Four Case Studies. In Feel, Sense, Design - INTERACT 2021 IFIP TC 13 Workshops, volume 13198 of Lecture Notes in Computer Science, pages 195-210. Springer.
 

2021

abstracts on (turn off)

C. Machado and J.C. Campos (2021)
Towards the integration of user interface prototyping and model-based development. In 2021 International Conference on Graphics and Interaction (ICGI), pages 1-8. IEEE.
 

K. Baumann, J.C. Campos, A. Dix, L. Nigay, P. Palanque, J. Vanderdonckt, G. van der Veer and B. Weyers (2021)
HCI-E² : HCI Engineering Education - For Developers, Designers and More. In C. Ardito et al., editor, Human-Computer Interaction - INTERACT 2021, volume 12936 of Lecture Notes in Computer Science, pages 542-547. Springer.
 

M.D. Harrison, P. Masci and J.C. Campos (2021)
Balancing the formal and the informal in user centred design. Interacting with Computers, 33(1):55-72, January.
This paper explores the role of formal methods as part of the user centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using "traditional" techniques for user evaluation. Formal analysis complements user evaluations. This approach enriches user centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non functional (e.g., paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser.
 

C. Silva, J. Vieira, J.C. Campos, R. Couto and A.N. Ribeiro (2021)
Development and validation of a Descriptive Cognitive Model for a Low Code Development Platform. Human Factors, 63(6):1012-1032.
This study proposes and evaluates a Descriptive Cognitive Model (DCM) for the identification of initial usability issues in a low-code development platform (LCDP). By applying the proposed DCM we were able to predict the interaction problems felt by first-time users of the LCDP.
   

2020

abstracts on (turn off)

J.C. Campos, C. Fayollas, M.D. Harrison, C. Martinie, P. Masci and P. Palanque (2020)
Supporting the analysis of safety critical user interfaces: an exploration of three formal tools. ACM Transactions on Computer-Human Interaction, 27(5), August.
Use error due to user interface design defects is a major concern in many safety critical domains, for example avionics and healthcare. Early detection of latent user interface problems can be facilitated by user centered design methods that integrate formal verification technologies. This paper considers the role that formal verification technologies can play in the context of user centered design by considering three existing tools: CIRCUS, PVSio-web, and IVY. These tools have been developed to support the model based analysis of critical user interfaces. They have their foundations in existing formal verification technologies, but each of them is focused towards particular issues relating to user interface design. The paper explores the different phases of the user centered design process and the extent to which each of these tools supports these phases. Criteria are developed for assessing their role at each stage of the design process. The results of the evaluation provide guidance to developers to help choose the most appropriate tool based on their analysis needs while at the same time setting challenges for future developments.
   

A. Canny, D. Navarre, J.C. Campos and P. Palanque (2020)
Model-Based Testing of Post-WIMP Interactions Using Petri-nets. In E. Sekerinski et al., editor, Formal Methods. FM 2019 International Workshops, volume 12232 of Lecture Notes in Computer Science, pages 486-502. Springer.
   

2019

abstracts on (turn off)

J. Ara�jo, R. Couto and J.C. Campos (2019)
A Generator of User Interface Prototypes for the IVY Workbench. In ICGI 2019 -- International Conference on Graphics and Interaction, pages 32-39. IEEE.
   

M.D. Harrison, P. Masci and J.C. Campos (2019)
Verification Templates for the Analysis of User Interface Software Design. IEEE Transactions on Software Engineering, 45(8):802-822, August.
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.
   

C. Silva, P. Masci, Y. Zhang, P. Jones and J.C. Campos (2019)
A Use Error Taxonomy for Improving Human-Machine Interface Design in Medical Devices. ACM SIGBED Review (Special Issue on Medical Cyber Physical Systems - MCPS'18), 16(2):24-30, July.
Use error is one of the leading causes of medical device incidents. It is crucial for all stakeholders to have a unified means to better understand, classify, communicate, and prevent/avoid medical device use errors. In this paper, we present our ongoing work on developing a new use error taxonomy for medical devices that has the potential to enable fine-grained analysis of use errors and their root causes in system design. Our ultimate goal is to create a generic framework that can be used by medical device designers to better identify effective design solutions to mitigating use errors.
   

R. Couto and J.C. Campos (2019)
High assurance on Cyber-Physical Interactive Systems. In HCI Engineering 2019 - Methods and Tools for Advanced Interactive Systems and Integration of Multiple Stakeholder Viewpoints, pages 46-50.
 

J.C. Campos and M.D. Harrison (2019)
Formal verification of interactive computing systems: opportunities and challenges. In HCI Engineering 2019 - Methods and Tools for Advanced Interactive Systems and Integration of Multiple Stakeholder Viewpoints, volume 2503 of CEUR Workshop Proceedings, pages 69-75.
 

R. Couto and J.C. Campos (2019)
IVY 2 - A model-based analysis tool. In The 11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems - EICS 2019, pages 5:1--5:6. ACM.
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.
 

D. Distante, M. Winckler, R. Bernhaupt, J. Bowen, J.C. Campos, F. M�ller, P. Palanque, J. Van den Bergh, B. Weyers and A. Voit (2019)
Trends on Engineering Interactive Systems: An Overview of Works Presented in Workshops at EICS 2019. In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 22:1--22:6. ACM.
 

M.D. Harrison, L. Freitas, M. Drinnan, J.C. Campos, P. Masci, C. di Maria and M. Whitaker (2019)
Formal Techniques in the Safety Analysis of Software Components of a new Dialysis Machine. Science of Computer Programming, 175:17-34, April.
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.
   

2018

abstracts on (turn off)

R. Couto, J.C. Campos, N. Macedo and A. Cunha (2018)
Improving the Visualization of Alloy Instances. In Integrated Development Environment 2018 (F-IDE 2018), volume 284 of Electronic Proceedings in Theoretical Computer Science, pages 37-52.
Alloy is a lightweight formal specification language, supportedby an IDE, which has proven well-suited for reasoning aboutsoftware design in early development stages. The IDE provides a Visualizerthat produces graphical representations of analysis results, whichis essential for the proper validation of the model. Alloy is a rich languagebut inherently static, so behavior needs to be explicitly encodedand reasoned about. Even though this is a common scenario, the Visualizerpresents limitations when dealing with such models. The maincontribution of this paper is a principled approach to generate instancevisualizations, which improves the current Alloy Visualizer, focusing onthe representation of behavior.
   

M.D. Harrison, P. Masci and J.C. Campos (2018)
Formal modelling as a component of user centred design. In M. Mazzara, I. Ober and G. Sala�n, editors, Software Technologies: Applications and Foundations, volume 11176 of Lecture Notes in Computer Science, pages 274-289. Springer.
User centred design approaches typically focus understanding on context and producing sketch designs. These sketches are often non functional (e.g., paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The sketch design of a device is refined into a specification that is then analysed using formal techniques, thus providing a systematic approach to checking plausibility and consistency during early design stages. Once analysed, a further prototype is constructed using an executable form of the specification, providing the next candidate for evaluation with potential users.The technique is illustrated through an example based on a pill dispenser.
   

R. Couto and J.C. Campos (2018)
Improving traces visualisation through layout managers. In ICGI 2018 - 1st International Conference on Graphics and Interaction, pages 41-48. IEEE.
Alloy supports reasoning about software designs in early development stages. It is composed of a modelling language and a tool that is able to find valid instances of the model. Alloy is able to produce graphical representations of analysis results, which is essential for their interpretation. In previous work we have improved the representations with the usage of layout managers. Here, we further extend that work by presenting the improvements on the approach, and by introducing a new case study to analyse the contribution of layout managers, and to support validation trough a user study.
   

C. Silva and J.C. Campos (2018)
Towards a Simulation-Based Medical Education Platform for PVSio-Web. In ICGI 2018 - 1st International Conference on Graphics and Interaction. IEEE.
Interface design flaws are often at the root cause of use errors in medical devices. Medical incidents are seldom reported, thus hindering the understanding of the incident contributing factors. Moreover, when dealing with a use error, both novices and expert users often blame themselves for insufficient knowledge rather than acknowledge deficiencies in the device. Simulation-Based Medical Education (SBME) platforms can provide appropriate training to professionals, especially if the right incentives to keep training are in place. In this paper, we present a new SBME, particularly target at training interaction with medical devices such as ventilators and infusion pumps. Our SBME functions as a game mode of the PVSio-web, a graphical environment for design, evaluation, and simulation of interactive (human-computer) systems. An analytical evaluation of our current implementation is provided, by comparing the features on our SMBE with a set of requirements for game-based medical simulators retrieved from the literature. By being developed in a free, open source platform, our SMBE is highly accessible and can be easily adapted to specific use cases, such a specific hospital with a defined set of medical devices.
   

J.C. Campos and N. Sousa (2018)
The MAL Interactors Animator: Supporting model validation through animation. In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 11:1--11:7. ACM.
The IVY workbench is a model checking based tool for the analysis of interactive systems designs. Experience, however, shows that there is a need to complement the analytic power of model checking with support for model validation and verification results’ interpretation. Animation of the model provides this support by allowing the iterative exploration of the model. This paper introduces a new model animation plugin for the IVY workbench. The plugin (AniMAL) complements the modelling and verification capabilities of IVY by providing users with the possibility to interact directly with the model.
   

P Masci, Y Zhang, P Jones and JC Campos (2018)
Extending STPA to Improve the Analysis of User Interface Software in Medical Devices. STAMP Workshop 2018.
We present a method to enhance the standard STPA causal factors categories and tailor them to the analysis of user interface software in medical devices. Our method builds on usability design principles, and aims to facilitate the analysis of specific use-related aspects of a software design that could impact the safety of a medical device. Initial evaluation of the method on realistic case studies indicates that our method facilitates the detection of latent software issues that can be hard to identify with the standard STPA categories.
 

2017

abstracts on (turn off)

M.D. Harrison, M. Drinnan, J.C. Campos, P. Masci, L. Freitas, C. di Maria and M. Whitaker (2017)
Safety analysis of software components of a dialysis machine using model checking. In Formal Aspects of Component Software, volume 10487 of Lecture Notes in Computer Science, pages 137-154. Springer.
The paper describes the practical use of a model checking technique to contribute to the risk analysis of a new paediatric dialysis machine. The formal analysis focuses on one component of the system, namely the table-driven software controller which drives the dialysis cycle and deals with error management. The analysis provided evidence of the verification of risk control measures relating to the software component. The paper describes the productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and an analyst who had experience of using the formal analysis tools. There were two aspects to this dialogue. The first concerned the translation of safety requirements so that they preserved the meaning of the requirement. The second involved understanding the relationship between the software component under analysis and the broader concern of the system as a whole. The paper focuses on the process, highlighting how the team recognised the advantages over a more traditional testing approach.
   

M. Pinto, M. Gon�alves, P. Masci, and J.C. Campos (2017)
TOM: a Model-Based GUI Testing framework. In Formal Aspects of Component Software, volume 10487 of Lecture Notes in Computer Science, pages 155-161. Springer.
Applying model-based testing to interactive systems enables the systematic testing of the system by automatically simulating user actions on the user interface. It reduces the cost of (expensive) user testing by identifying implementations errors without the involvement of human users, but raises a number of specific challenges, such as how to achieve good coverage of the actual use of the system during the testing process. This paper describes TOM, a model-based testing framework that uses a combination of tools and mutation testing techniques to maximize testing of user interface behaviors.
   

M.D. Harrison, P. Masci, J.C. Campos and P. Curzon (2017)
Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. IEEE Transactions on Human-Machine Systems, 47(6):834-846, December.
 

P. Masci, Y. Zhang, P. Jones and J.C. Campos (2017)
A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices. In Software Engineering and Formal Methods (SEFM'17), volume 10469 of Lecture Notes in Computer Science, pages 284-299. Springer.
Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson’s System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that 1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and 2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).
   

J.C. Campos, C. Fayollas, M. Gon�alves, C. Martinie, D. Navarre, P. Palanque and M. Pinto (2017)
A "More Intelligent" Test Case Generation Approach through Task Models Manipulation. Proceedings of the ACM on Human Computer Interaction, 1(EICS):9:1-9:20.
Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the e ectiveness factor of usability directly refers to this capability. Assessing e ectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of e ectiveness of interactive applications. To this end we resort to two main elements: an exhaustive description of users’ activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information ...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance (both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications.
   

Machado, M., Couto, R. and Campos, J.C. (2017)
MODUS: Model-based User Interfaces Prototyping. In Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 111--116. ACM.
Model-based methodologies, supported by automatic generation, have been proposed as a solution to reduce software development costs. In the case of interactive computing systems specific challenges arise. On the one hand, a high level of automation requires the use of detailed models, which is contrary to the iterative development process, based on the progressive refinement of user interface mockups, typical of user centered development processes. On the other hand, layered software architectures imply a distinction between the models used in the business logic and in the user interface, raising consistency problems between the models at each level. This article proposes a tool supported approach to user interface generation directly from the architectural models of the business logic. In many situations, user interfaces provide similar features inside a specific domain. The identification of the application domain is thus a key factor in supporting the automation of the generation process.
   

Harrison, M.D., Masci, P.M., Campos, J.C. and Curzon, P. (2017)
The specification and analysis of use properties of a nuclear control system. In Weyers, B., Palanque, P., Bowen, J. and Dix, A., editors, The Handbook on Formal Methods in Human Computer Interaction, Human-Computer Interaction Series, chapter 14. Springer.
This chapter explores a layered approach to the analysis of the Nuclear Power Plant Control System described in Chap. 4. A model is specified to allow the analysis of use-centred properties based on generic templates. User interface properties include the visibility of state attributes, the clarity of the mode structure and the ease with which an action can be recovered from. Property templates are used as heuristics to ease the construction of requirements for the control system interface.
 

Campos, J.C., Abade, T., Silva, J.L. and Harrison, M.D. (2017)
Don't Go In There! Using the APEX framework in the design of ambient assisted living systems. Journal of Ambient Intelligence and Humanized Computing, 8(4):551-566.
An approach to design Ambient Assisted Living systems is presented, which is based on APEX, a framework for prototyping ubiquitous environments. The approach is illustrated through the design of a smart environment within a care home for older people. Prototypes allow participants in the design process to experience the proposed design and enable developers to explore design alternatives rapidly. APEX provides the means to explore alternative environment designs virtually. The prototypes developed with APEX offered a mediating representation, allowing users to be involved in the design process. A group of residents in a city-based care home were involved in the design. The paper describes the design process as well as lessons learned for the future design of AAL systems.
     

Fayollas, C., Martinie, C., Palanque, P., Masci, P., Harrison, M.D., Campos, J.C. and Silva, S.R. (2017)
Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. In Proceedings of the Third Workshop on Formal Integrated Development Environment, volume 240 of Electronic Proceedings in Theoretical Computer Science, pages 1-19.
Critical human-machine interfaces are present in many systems including avionics systems and medical devices. Use error is a concern in these systems both in terms of hardware panels and input devices, and the software that drives the interfaces. Guaranteeing safe usability, in terms of buttons, knobs and displays is now a key element in the overall safety of the system. New integrated development environments (IDEs) based on formal methods technologies have been developed by the research community to support the design and analysis of high-confidence human-machine interfaces. To date, little work has focused on the comparison of these particular types of formal IDEs. This paper compares and evaluates two state-of-the-art toolkits: CIRCUS, a model-based development and analysis tool based on Petri net extensions, and PVSio-web, a prototyping toolkit based on the PVS theorem proving system.
 

M.D. Harrison, P. Masci, J.C. Campos and P. Curzon (2017)
Demonstrating that medical devices satisfy user related safety requirements. In Software Engineering in Healthcare (FHIES/SEHC 2014), volume 9062 of Lecture Notes in Computer Science, pages 113-128. Springer.
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.
   

P. Machado, R. Couto and J.C. Campos (2017)
Um editor tabular para modelação de interfaces. In Atas do EPCGI 2017 - 24o. Encontro Português de Computação Gráfica e Interação, pages 243-244.

R. Couto, A.N. Ribeiro and J.C. Campos (2017)
Avalia��o de Usabilidade da ferramenta uCat. In Atas do EPCGI 2017 - 24o. Encontro Português de Computação Gráfica e Interação, pages 239-240.

R. Couto, A.N. Ribeiro and J.C. Campos (2017)
De Requisitos a Prot�tipos de UI: Uma Abordagem Semi Automatizada. In Atas do EPCGI 2017 - 24� Encontro Portugu�s de Computa��o Gr�fica e Intera��o, pages 237-238.

2016

abstracts on (turn off)

Luyten, K., Palanque, P., Campos, J.C. and Schmidt, A., editor(s) (2016)
Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '16. ACM.
 

J.C. Campos, C. Fayollas, C. Martinie, D. Navarre, P. Palanque and M. Pinto (2016)
Systematic Automation of Scenario-Based Testing of User Interfaces. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 138-148. ACM.
   

M. Harrison, J.C. Campos, R. Ruksenas and P. Curzon (2016)
Modelling information resources and their salience in medical device design. In Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pages 194-203. ACM.
The paper describes a model that includes an explicit description of the information resources that are assumed to guide use, enabling a focus on properties of "plausible interactions". The information resources supported by an interactive system should be designed to encourage the correct use of the system. These resources signpost a user's interaction, helping to achieve desired goals. Analysing assumptions about information resource support is particularly relevant when a system is safety critical that is when interaction failure consequences could be dangerous, or walk-up-and-use where interaction failure may lead to reluctance to use with expensive consequences. The paper shows that expressing these resource constraints still provides a wider set of behaviours than would occur in practice. A resource may be more or less salient at a particular stage of the interaction and as a result potentially overlooked. For example, the resource may be accessible but not used because it does not seem relevant to the current goal. The paper describes how the resource framework can be augmented with additional information about the salience of the assumed resources. A medical device that is in common use in many hospitals is used as illustration.
   

R. Couto, A.N. Ribeiro and J.C. Campos (2016)
Validating an approach to formalize use cases with ontologies. In Proceedings of the 13th International Workshop on Formal Engineering Approaches to Software Components and Architectures, volume 205 of Electronic Proceedings in Theoretical Computer Science, pages 1-15. Open Publishing Association.
Use case driven development methodologies put use cases at the center of the software development process. However, in order to support automated development and analysis, use cases need to be appropriately formalized. This will also help guarantee consistency between requirements specifications and the developed solutions. Formal methods tend to suffer from take up issues, as they are usually hard to accept by industry. In this context, it is relevant not only to produce languages and approaches to support formalization, but also to perform their validation. In previous works we have developed an approach to formalize use cases resorting to ontologies. In this paper we present the validation of one such approach. Through a three stage study, we evaluate the acceptance of the language and supporting tool. The first stage focusses on the acceptance of the process and language, the second on the support the tool provides to the process, and finally the third one on the tool's usability aspects. Results show test subjects found the approach feasible and useful and the tool easy to use.
 

J.C. Campos, M. Sousa, M. Alves and M.D. Harrison (2016)
Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems, 46(2):303-316.
This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.
   

2015

abstracts on (turn off)

M. Harrison, J.C. Campos, P. Masci and P. Curzon (2015)
Templates as heuristics for proving properties of medical devices. In 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". ACM.
 

J.C. Campos, J.L. Silva and M. Harrison (2015)
Supporting the Design of an Ambient Assisted Living System Using Virtual Reality Prototypes. In Ian Cleland, Luis Guerrero and Jos� Bravo, editors, Ambient Assisted Living. ICT-based Solutions in Real Life Situations, volume 9455 of Lecture Notes in Computer Science, pages 49-61. Springer.
   

M. Machado, J.C. Campos and R. Couto (2015)
MODUS: uma metodologia de prototipagem de interfaces baseada em modelos. In Inforum 2015: Atas do 7� Simp�sio Nacional de Inform�tica, pages 17-32. UBI - Universidade da Beira Interior.
A interface de utilizador � essencial para o sucesso de uma aplica��o, ora a sua implementa��o requer tempo e esfor�o. Metodologias baseadas em modelos suportadas por uma gera��o autom�tica t�m sido propostas como solu��o para reduzir os custos de desenvolvimento. No entanto, um elevado n�vel de automa��o nestas abordagens requer o uso de modelos detalhados da interface, originando complica��es. Por um lado, esta perspetiva � contr�ria a uma conce��o baseada no progressivo refinamento de mockups, t�pica do desenvolvimento de interfaces. Por outro lado, obriga uma distin��o entre os modelos utilizados na l�gica de neg�cio e na interface. Este artigo prop�e uma abordagem para gerar a interface de utilizador baseada diretamente em modelos estruturais da l�gica de neg�cio. A identifica��o do dom�nio de aplica��o � um factor chave da metodologia, permitindo automatizar o processo de gera��o. Por sua vez a separa��o entre conte�do e forma favorece o refinamento iterativo das interfaces geradas.
 

T. Abade, J.C. Campos, R. Moreira, C.C.L. Silva and J.L. Silva (2015)
Immersiveness of Ubiquitous Computing Environments Prototypes: A case study. In N. Streitz and P. Markopoulos, editors, Distributed, Ambient and Pervasive Interactions, volume 9189 of Lecture Notes in Computer Science, pages 237-248. Springer.
     

J.C. Campos, P. Masci, P. Curzon and M.D. Harrison (2015)
Layers, resources and property templates in the specification and analysis of two interactive systems. In Proceedings of the Workshop on Formal Methods in Human Computer Interaction (FoMHCI) 2015, pages 38-43. Universitätsbibliothek, RWTH Aachen University.
The paper briefly explores a layered approach to the analysis of two interactive systems (Nuclear Control and Air Traffic Control), indicating how the analysis enables exploration of the particular features emphasised by the use cases relating to the examples. These features relate to the interactive behaviour of the systems. To facilitate the analysis, property templates are proposed as heuristics for developing appropriate requirements for the respective user interfaces.
 

R. Couto, A.N. Ribeiro and J.C. Campos (2015)
The Modelery: A Model-Based Software Development Repository. International Journal of Web Information Systems, 11(2):205-225.
   

D. Almeida, J.C. Campos, J. Saraiva and J.C. Silva (2015)
Towards a Catalog of Usability Smells. In ACM SAC 2015 proceedings - Volume I: Artificial Intelligence and Agents, Distributed Systems, and Information Systems, pages 175-181. ACM.
This paper presents a catalog of smells in the context of interactive applications. These so-called usability smells are indicators of poor design on an application's user interface, with the potential to hinder not only its usability but also its maintenance and evolution. To eliminate such usability smells we discuss a set of program/usability refactorings. In order to validate the presented usability smells catalog, and the associated refactorings, we present a preliminary empirical study with software developers in the context of a real open source hospital management application. Moreover, a tool that computes graphical user interface behaviour models, giving the applications' source code, is used to automatically detect usability smells at the model level.
   

M.D. Harrison, J.C. Campos and P. Masci (2015)
Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering, 11(2):95-111, June.
The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking a battery of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting but differ in a number of respects as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.
       

J. Lamas, C.C.L. Silva, M. Silva, S. Mouta, J.C. Campos, J.A. Santos (2015)
Measuring end-to-end delay in real-time auralisation systems. In Euronoise - 10th European Congress and Exposition on Noise Control Engineering, pages 791-796. EAA-NAG-ABAV.
One of the major challenges in the development of an immersive system is handling the delay between the tracking of the user's head position and the updated projection of a 3D image or auralised sound, also called end-to-end delay. Excessive end-to-end delay can result in the general decrement of the “feeling of presence”, the occurrence of motion sickness and poor performance in perception-action tasks. These latencies must be known in order to provide insights on the technological (hardware/software optimization) or psychophysical (recalibration sessions) strategies to deal with them. Our goal was to develop a new measurement method of end-to-end delay that is both precise and easily replicated. We used a Head and Torso simulator (HATS) as an auditory signal sensor, a fast response photo-sensor to detect a visual stimulus response from a Motion Capture System, and a voltage input trigger as real-time event. The HATS was mounted in a turntable which allowed us to precisely change the 3D sound relative to the head position. When the virtual sound source was at 90 azimuth, the correspondent HRTF would set all the intensity values to zero, at the same time a trigger would register the real-time event of turning the HATS 90 azimuth. Furthermore, with the HATS turned 90 to the left, the motion capture marker visualization would fell exactly in the photo-sensor receptor. This method allowed us to precisely measure the delay from tracking to displaying. Moreover, our results show that the method of tracking, its tracking frequency, and the rendering of the sound reflections are the main predictors of end-to-end delay.
   

2014

abstracts on (turn off)

J.C. Campos, G. Doherty and M.D. Harrison (2014)
Analysing interactive devices based on information resource constraints. International Journal of Human-Computer Studies, 72(3):284-297, March.
Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.
   

J.L. Silva, J.C. Campos and M.D Harrison (2014)
Prototyping and Analysing Ubiquitous Computing Environments using Multiple Layers. International Journal of Human-Computer Studies, 72(5):488-506, May.
If ubiquitous computing (ubicomp) is to enhance physical environments then early and accurate assessment of alternative solutions will be necessary to avoid costly deployment of systems that fail to meet requirements. This paper presents APEX, a prototyping framework that combines a 3D Application Server with a behaviour modeling tool. The contribution of this framework is that it allows exhaustive analysis of the behaviour models that drive the prototype while at the same time enabling immersive exploration of a virtual environment simulating the proposed system. The development of prototypes is supported through three layers: a simulation layer (using OpenSimulator); a modelling layer (using CPN Tools) and a physical layer (using external devices and real users). APEX allows movement between these layers to analyse different features, from user experience to user behaviour. The multi layer approach makes it possible to express user behaviour in the modelling layer, provides a way to reduce the number of real users needed by adding simulated avatars, and supports user testing of hybrids of virtual and real components as well as exhaustive analysis. This paper demonstrates the approach by means of an example, placing particular emphasis on the simulation of virtual environments, low cost prototyping and the formal analysis capabilities.
   

T. Gomes, T. Abade, J.C. Campos, M.D. Harrison and J.L. Silva (2014)
A Virtual Environment based Serious Game to Support Health Education. EAI Endorsed Transactions on Ambient Systems, 14(3):e5, March.
APEX was developed as a framework for ubiquitous computing (ubicomp) prototyping through virtual environments. In this paper the framework is used as a platform for developing a serious game designed to instruct and to inform. The paper describes the Asthma game, a game aimed at raising awareness among children of asthma triggers in the home. It is designed to stimulate a healthier life-style for those with asthma and respiratory problems. The game was developed as the gamification of a checklist for the home environment of asthma patients.
   

C.E. Silva and J.C. Campos (2014)
Characterizing the Control Logic of Web Applications' User Interfaces. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 263-276. Springer.
In order to develop an hybrid approach to the Reverse Engineer of Web applications, we need first to understand how much of the control logic of the user interface can be obtained from the analysis of event listeners. To that end, we have developed a tool that enables us to perform such analysis, and applied it to the implementation of the one thousand most widely used Websites (according to Alexa Top Sites). This paper describes our approach for analyzing the user interface layer of those Websites, and the results we got from the analysis. The conclusions drawn from the exercise will be used to guide the development of the proposed hybrid reverse engineering tool.
     

R. Couto, A.N. Ribeiro and J.C. Campos (2014)
A Study on the Viability of Formalizing Use Cases. In 9th International Conference on the Quality of Information and Communications Technology, QUATIC 2014, pages 130-133. IEEE.
Use case scenarios are known as powerful means for requirements specification. On the one hand, they join in the same modelling space the expectations of the stakeholders and the needs of the developers involved in the process. On the other hand, they describe the desired high level functionalities. By formalizing these descriptions we are able to extract relevant information's from them. Specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. This paper addresses the transformation of use case descriptions expressed in a Controller Natural Language into an ontology expressed in the Web Ontology Language (OWL), as well as the query process for such information. It reports on a study aimed at validating our approach and our tool with real users. A preliminary set of results is discussed.
   

R. Couto, A.N. Ribeiro and J.C. Campos (2014)
The Modelery: A Collaborative Web Based Repository. In Computational Science and Its Applications - ICCSA 2014, volume 8584 of Lecture Notes in Computer Science, pages 1-16. Springer.
Software development processes are known to produce a large set of artifacts such as models, code and documentation. Keeping track of these artifacts without supporting tools is not easy, and making them available to others can be even harder. Standard version control systems are not able to solve this issue. More than keeping track of versions, a system to help organize and make artifacts available in meaningful ways is needed. In this paper we review a number of alternative systems, and present the requirements and the implementation of a collaborative web repository which we developed to solve this issue.
   

T. Abade, T. Gomes, J.L. Silva and J.C. Campos (2014)
Design and Evaluation of a Smart Library using the APEX Framework. In N. Streitz and P. Markopoulos, editors, Distributed, Ambient, and Pervasive Interactions, volume 8530 of Lecture Notes in Computer Science, pages 307-318. Springer.
User experience is a key point for successful ubiquitous computing (ubicomp) environments. The envisaged design should be explored as soon as possible to anticipate potential user problems, thus reducing re-design costs. The development of ubicomp environments’ prototypes might help, providing feedback on the users’ reaction to the environments. This paper describes the design and evaluation of ubicomp environments using APEX, a rapid prototyping framework providing user experience via a 3D application server and connected physical devices. APEX prototypes allow users to explore and experience many characteristics of a proposed design, in a virtual world. The paper focus in particular the design and evaluation of a smart library in the APEX framework.
     

A.I. Sampaio and J.C. Campos (2014)
Towards a Framework for Adaptive Web Applications. In C. Stephanidis, editor, HCI International 2014 - Posters' Extended Abstracts, Part I, volume 434 of Communications in Computer and Information Science, pages 240-245. Springer.
We have developed a framework to support adaptive elements in Web pages. In particular we focus on adaptive menus. Developers are able to define rules for menu adaptation according to the features of the device and browser in use. This paper briefly describes the selected adaptation patterns and their implementation.
     

T. Gomes, T. Abade, J.C. Campos, M.D. Harrison and J.L. Silva (2014)
Rapid Development of First Person Serious Games using the APEX Platform: The Asthma Game. In ACM SAC 2014 proceedings - Volume I: Artificial Intelligence & Agents, Distributed Systems, and Information Systems, pages 169-174. ACM.
Serious games combine a ludic component with instructive and formative goals. They aim to educate and train through play. This paper explores the use of a development framework for dynamic virtual environments to develop serious games. The framework (APEX) was originally developed to prototype ubiquitous computing (ubicomp) environments. Here it is used to develop a first person serious game: the Asthma Game. This game aims to teach children with asthma how to act to prevent attacks by drawing attention to asthma triggers in the home, and by providing information about how to avoid them. Besides the description of the game, results about the viability and utility of the approach are also discussed.
     

J.C. Campos (2014)
High assurance interactive computing systems. In J. Ziegler, J. C. Campos and L. Nigay, editors, HCI Engineering: Charting the Way towards Methods and Tools for Advanced Interactive Systems, pages 39-42.
If interactive computing systems development is to be considered an engineering discipline, we need methods and tools to help us reason about and predict the quality of systems, from early in the design process. This paper provides a brief overview of work we have been carrying out in the general area of evaluating and ensuring the quality of interactive computing systems. Some of the work currently being carried out is also discussed. Discussed approaches range from the formal verification of user interface models through model checking, to the reverse engineering and model based testing of implemented interactive computing systems.
   

R. Couto, A.N. Ribeiro and J.C. Campos (2014)
Application of Ontologies in Identifying Requirements Patterns in Use Cases. In 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2014), volume 147 of Electronic Proceedings in Theoretical Computer Science, pages 62-76.
Use case specifications have successfully been used for requirements description. They allow joining, in the same modeling space, the expectations of the stakeholders as well as the needs of the software engineer and analyst involved in the process. While use cases are not meant to describe a system's implementation, by formalizing their description we are able to extract implementation relevant information from them. More specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. In the paper we propose the transformation of Use Case descriptions expressed in a Controlled Natural Language into an ontology expressed in the Web Ontology Language (OWL). OWL's query engines can then be used to identify requirements patterns expressed as queries over the ontology. We describe a tool that we have developed to support the approach and provide an example of usage.
   

M. Sousa, J.C. Campos, M. Alves and M.D. Harrison (2014)
Formal Verification of Safety-Critical User Interfaces: a space system case study. In Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, pages 62-67. AAAI Press.
Safe operation of safety critical systems depends on appropriate interactions between the human operator and the computer system. Specification of such safety-critical systems is fundamental to enable exhaustive and automated analysis of operator system interaction. In this paper we present a structured, comprehensive and computer-aided approach to formally specify and verify user interfaces based on model checking techniques.
   

J.C. Silva, J.C. Campos, J. Saraiva and J.L. Silva (2014)
An approach for graphical user interface external bad smells detection. In New Perspectives in Information Systems and Technologies, vol. 2, volume 276 of Advances in Intelligent Systems and Computing, pages 199-205. Springer.
In the context of an effort to develop methodologies to support the evaluation of interactive system, this paper investigates an approach to detect graphical user interface external bad smells. Our approach consists in detecting user interface external bad smells through model-based reverse engineering from source code. Models are used to define which widgets are present in the interface, when can particular graphical user interface (GUI) events occur, under which conditions, which system actions are executed, and which GUI state is generated next. From these models we obtain metrics that can later be used to identify the smells.
   

J.M. Machado and J.C. Campos (2014)
Development of Dependable Controllers in the Context of Machines Design. In Modern Methods of Construction Design, Lecture Notes in Mechanical Engineering, pages 125-131. Springer.
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.
   

J. Ziegler, J.C. Campos and L. Nigay (2014)
HCI engineering: Charting the way towards methods and tools for advanced interactive systems. In Proceedings of the 2014 ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2014), pages 299-300. ACM.
This workshop intends to establish the basis of a roadmap addressing engineering challenges and emerging themes in HCI. Novel forms of interaction and new application domains involve aspects that are currently not sufficiently covered by existing methods and tools. The workshop will serve as a venue to bring together researchers and practitioners interested the Engineering of Human- Computer Interaction and in contributing to the definition of a roadmap for the field. The intention is to continue work on the roadmap in follow-up workshops as well as in the IFIP Working Group on User Interface Engineering.
 

2013

abstracts on (turn off)

M.D. Harrison, P. Masci, J.C. Campos and P. Curzon (2013)
Automated theorem proving for the systematic analysis of an infusion pump. Electronic Communications of the EASST, 69: Formal Methods for Interactive Systems 2011. (ISSN: 1863-2122)
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.
 

C. Silva, C. Mendon�a, S. Mouta, R. Silva, J.C. Campos and J. Santos (2013)
Depth cues and perceived audiovisual synchrony of biological motion. PLoS ONE, 8(11):e80096, November.
Background: Due to their different propagation times, visual and auditory signals from external events arrive at the human sensory receptors with a disparate delay. This delay consistently varies with distance, but, despite such variability, most events are perceived as synchronic. There is, however, contradictory data and claims regarding the existence of compensatory mechanisms for distance in simultaneity judgments. Principal Findings: In this paper we have used familiar audiovisual events – a visual walker and footstep sounds – and manipulated the number of depth cues. In a simultaneity judgment task we presented a large range of stimulus onset asynchronies corresponding to distances of up to 35 meters. We found an effect of distance over the simultaneity estimates, with greater distances requiring larger stimulus onset asynchronies, and vision always leading. This effect was stronger when both visual and auditory cues were present but was interestingly not found when depth cues were impoverished. Significance: These findings reveal that there should be an internal mechanism to compensate for audiovisual delays, which critically depends on the depth information available.
   

T. Gomes, T. Abade, J.L. Silva and J.C. Campos (2013)
Desenvolvimento de Jogos Educativos na plataforma APEX: O Jogo da Asma. In Lu�s Magalh�es and Beatriz Santos, editors, Atas da Confer�ncia Intera��o 2013, pages 90-97. Universidade de Tr�s-os-Montes e Alto Douro.
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 se 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.
 

T. Abade, T. Gomes, J.L. Silva and J. C. Campos (2013)
Avalia��o de Ambientes Ub�quos na Plataforma APEX. In Lu�s Magalh�es and Beatriz Santos, editors, Atas da Confer�ncia Intera��o 2013, pages 177-178. Universidade de Tr�s-os-Montes e Alto Douro.
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.
 

P.J. Cruz and J.C. Campos (2013)
Ambiente de gera��o, muta��o e execu��o de casos de teste para aplica��es Web. In Lu�s Magalh�es and Beatriz Santos, editors, Atas da Confer�ncia Intera��o 2013, pages 45-52. Universidade de Tr�s-os-Montes e Alto Douro.
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.
 

T. Gomes, T. Abade, M.D. Harrison, J.L. Silva and J.C. Campos (2013)
Developing Serious Games With The APEX Framework. In Proceedings of the Workshop on "Ubiquitous games and gamification for promoting behavior change and wellbeing", pages 37-40.
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.
 

C.E. Silva and J.C. Campos (2013)
Combining Static and Dynamic Analysis for the Reverse Engineering of Web Applications. In P. Forbrig, P. Dewan, M. Harrison, K. Luyten, C. Santoro and S.D.J. Barbosa, editors, Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2013), pages 107-112. ACM.
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.
   

J.C. Silva, J.L. Silva, J.C. Campos and J.A. Saraiva (2013)
Uma Abordagem para a Gera��o de Casos de Teste Baseada em Modelos. In Sistemas e Tecnologias de Informa��o (CISTI 2013), volume 2, pages 142-146. AISTI.
   

J.C. Campos and J. Machado (2013)
A Specification Patterns System for Discrete Event Systems' Analysis. International Journal of Advanced Robotic Systems, 10:315.
As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express properties of a system's behavior is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skillful process. Errors in this step of the process can create serious problems since a false sense of safety is gained with the analysis. However, when compared to the effort put into developing and applying modeling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements.
   

S. Moreira, R. Jos� and J.C. Campos (2013)
An empirical study on immersive prototyping dimensions. In M. Kurosu, editor, Human-Computer Interaction: Human-Centred Design Approaches, Methods, Tools and Environments, volume 8004 of Lecture Notes in Computer Science, pages 421-430. Springer.
     

L. Oliveira, A.N. Ribeiro and J.C. Campos (2013)
The Mobile Context Framework: providing context to mobile applications. In N. Streitz and C. Stephanidis, editors, Distributed, Ambient and Pervasive Interactions, volume 8028 of Lecture Notes in Computer Science, pages 144-153. Springer.
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.
   

R. Couto, A.N. Ribeiro and J.C. Campos (2013)
MapIt: A model based pattern recovery tool. In R.J. Machado, R.S.P. Maciel, J. Rubin and G. Botterweck, editors, Model-Based Methodologies for Pervasive and Embedded Software, volume 7706 of Lecture Notes in Computer Science, pages 19-37. Springer.
Design patterns provide a means to reuse proven solutions during development, but also to identify good practices during analysis. These are particularly relevant in complex and critical software, such as is the case of ubiquitous and pervasive systems. Model Driven Engineering (MDE) presents a solution for this problem, with the usage of high level models. As part of an effort to develop approaches to the migration of applications to mobile contexts, this paper reports on a tool that identifies design patterns in source code. Code is transformed into both platform specific and independent models, and from these design patterns are inferred. MapIt, the tool which implements these functionalities is described.
   

2012

abstracts on (turn off)

R. Couto, A.N. Ribeiro and J.C. Campos (2012)
A patterns based reverse engineering approach for Java source code. In 35th Annual IEEE Software Engineering Workshop, pages 140-147. IEEE Computer Society.
The ever increasing number of platforms and languages available to software developers means that the software industry is reaching high levels of complexity. Model Driven Architecture (MDA) presents a solution to the problem of improving software development processes in this changing and complex environment. MDA driven development is based on models definition and transformation. Design patterns provide a means to reuse proven solutions during development. Identifying design patterns in the models of a MDA approach helps their understanding, but also the identification of good practices during analysis. However, when analyzing or maintaining code that has not been developed according to MDA principles, or that has been changed independently from the models, the need arises to reverse engineer the models from the code prior to patterns' identification. The approach presented herein consists in transforming source code into models, and infer design patterns from these models. Erich Gamma's cataloged patterns provide us a starting point for the pattern inference process. MapIt, the tool which implements these functionalities is described.
   

C.E. Silva and J.C. Campos (2012)
Can GUI implementation markup languages be used for modelling?. In Marco Winckler, Peter Forbrig and Regina Bernhaupt, editors, Human Centred Software Engineering (HCSE 2012), volume 7623 of Lecture Notes in Computer Science, pages 112-129. Springer.
The current diversity of available devices and form factors increases the need for model-based techniques to support adapting applications from one device to another. Most work on user interface modelling is built around declarative markup languages. Markup languages play a relevant role, not only in the modelling of user interfaces, but also in their implementation. However, the languages used by each community (modellers/developers) have, to a great extent evolved separately. This means that the step from concrete model to final interface becomes needlessly complicated, requiring either compilers or interpreters to bridge this gap. In this paper we compare a modelling language (UsiXML) with several markup implementation languages. We analyse if it is feasible to use the implementation languages as modelling languages.
 

S. Barbosa, J.C. Campos, R. Kazman, P. Palanque, M. Harrison and S. Reeves, editor(s) (2012)
Proceedings of the 4th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS'12. ACM, Copenhagen, Denmark.
 

M.D. Harrison, J.C. Campos, P. Masci and N. Thomas (2012)
Modelling and systematic analysis of interactive systems. In Matthew L. Bolton, Asaf Degani and Philippe Palanque, editors, Proceedings of the Workshop on Formal Methods in Human-Machine Interaction (Formal H), pages 25-28.
Two aspects of our research concern the application of formal methods in human-computer interaction. The first aspect is the modelling and analysis of interactive devices with a particular emphasis on the user device dyad. The second is the modelling and analysis of ubiquitous systems where there are many users, one might say crowds of users.The common thread of both is to articulate and prove properties of interactive systems, to explore interactive behaviour as it influences the user, with a particular emphasis on interaction failure. The goal is to develop systematic techniques that can be packaged in such a way that they can be used effectively by developers. This “whitepaper” will briefly describe the two approaches and their potential value as well as their limitations and development opportunities.
   

J.L. Silva, J.C. Campos and M.D. Harrison (2012)
Formal analysis of Ubiquitous Computing environments through the APEX framework. In ACM Symposium on Engineering Interactive Computing Systems (EICS2012), pages 131-140. ACM.
Ubiquitous computing (ubicomp) systems involve complex interactions between multiple devices and users. This complexity makes it difficult to establish whether: (1) observations made about use are truly representative of all possible interactions; (2) desirable characteristics of the system are true in all possible scenarios. To address these issues, techniques are needed that support an exhaustive analysis of a system's design. This paper demonstrates one such exhaustive analysis technique that supports the early evaluation of alternative designs for ubiquitous computing environments. The technique combines models of behavior within the environment with a virtual world that allows its simulation. The models support checking of properties based on patterns. These patterns help the analyst to generate and verify relevant properties. Where these properties fail then scenarios suggested by the failure provide an important aid to redesign. The proposed technique uses APEX, a framework for rapid prototyping of ubiquitous environments based on Petri nets. The approach is illustrated through a smart library example. Its benefits and limitations are discussed.
 

L. Freire, P.M. Arezes and J.C. Campos (2012)
A literature review about usability evaluation methods for e-learning platforms. Work: A Journal of Prevention, Assessment and Rehabilitation, 41:1038-1044.
 

J.C. Campos, J. Saraiva, C. Silva and J.C. Silva (2012)
GUIsurfer: A Reverse Engineering Framework for User Interface Software. In A.C. Telea, editor, Reverse Engineering - Recent Advances and Applications, chapter 2, pages 31-54. InTech.
   

2011

abstracts on (turn off)

J.C. Campos and S.A. Mendes (2011)
FlexiXML - A portable user interface rendering engine for UsiXML. In User Interface Extensible Markup Language - UsiXML'2011, pages 158-168. Thales Research and Technology. (ISBN: 978-2-9536757-1-9)
A considerable amount of effort in software development is dedicated to the user interaction layer.Given the complexity inherent to the development of this layer, it is important to be able to analyse the concepts and ideas being used in the development of a given user interface. This analysis should be performed as early as possible. Model- based user interface development provides a solution to this problem by providing developers with tools that enable both modeling, and reasoning about, user interfaces at different levels of abstraction. Of particular interest here, is the possibility of animating the models to generate actual user interfaces. This paper describes FlexiXML, a tool that performs the rendering and animation of user interfaces described in the UsiXML modeling language.
 

J.C. Campos and M.D. Harrison (2011)
Modelling and analysing the interactive behaviour of an infusion pump. Electronic Communications of the EASST, 45: Formal Methods for Interactive Systems 2011. (ISSN: 1863-2122)
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.
 

J.C. Campos and J. Machado (2011)
Supporting requirements formulation in software formal verification. In Ambrosio, A.M., Mattiello-Francisco, M.F., Batista, J.C., Barbosa, R. and Cancela, H., editors, Latin-American Symposium on Dependable Computing (LADC 2011) suplemental proceedings. INPE.
Formal verification tools such as model checkers have reached a stage were their applicability in the development process of dependable and safety critical systems has become viable. While the formal verification step in tools such as model checkers is fully automated, writing appropriate models and properties is a skillful process. In particular, a correct understanding of the logics used to express properties is needed to guarantee that properties correctly encode the original requirements. In this paper we illustrate how a patterns-based tool can help in simplifying the process of generating logical formulae from informally expressed requirements.
 

J. Machado and J.C. Campos (2011)
Partial Plant Models in Formal Verification of Industrial Automation Discrete Systems. In Ambrosio, A.M., Mattiello-Francisco, M.F., Batista, J.C., Barbosa, R. and Cancela, H., editors, Latin-American Symposium on Dependable Computing (LADC 2011) suplemental proceedings. INPE.
The use of a plant model for formal verification of Industrial Automation systems controllers is realistic because all automation systems are composed by a controller and a plant. Therefore, if the plant model is not used, there is a part of the system that is not considered. However, if there are some cases where the use of a plant model makes the formal verification results more realistic and robust, there are other cases where this does not always happen. Moreover, the discussion presented in this paper is related with the need of using a Plant Model considering, not all of the Plant Model, but Partial Plant models in order to facilitate formal verification tasks of Industrial Automation Discrete Event Systems Controllers.
 

A. Barbosa, A. Paiva and J.C. Campos (2011)
Test case generation from mutated task models. In Fabio Patern�, Kris Luyten, Frank Maurer, Prasun Dewan and Carmen Santoro, editors, ACM Symposium on Engineering Interactive Computing Systems (EICS 2011), pages 175-184. ACM. (ISBN: 978-1-4503-0778-9)
This paper describes an approach to the model-based testing of graphical user interfaces from task models. Starting from a task model of the system under test, oracles are generated whose behaviour is compared with the execution of the running system. The use of task models means that the effort of producing the test oracles is reduced. It does also mean, however, that the oracles are confined to the set of expected user behaviours for the system. The paper focuses on solving this problem. It shows how task mutations can be generated automatically, enabling a broader range of user behaviours to be considered. A tool, based on a classification of user errors, generates these mutations. A number of examples illustrate the approach.
 

J. Machado, E. Seabra, J.C. Campos, F. Soares and C. Le�o (2011)
Safe Controllers Design for Industrial Automation Systems. Computers & Industrial Engineering, 60(4):635-653, May. (ISSN: 0360-8352)
The de sign 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.
   

L. Freire, P.M. Arezes and J.C. Campos (2011)
A import�ncia das avalia��es qualitativas em sistemas E-learning. In P. Arezes, J.S. Baptista, M.P. Barroso, P. Carneiro, P. Cordeiro, N. Costa, R. Melo, A.S. Miguel and G.P. Perestrelo, editors, Occupational Safety and Hygiene (SHO 2011), pages 274-278.
� cada vez mais frequente encontrarem-se investiga��es sobre a usabilidade dos sistemas de E-learning. Como resultados destas investiga��es, parece ser claro que grande parte delas aponta para a necessidade de uma discuss�o cr�tica acerca de m�todos para avalia��o de usabilidade espec�ficos para os sistemas educativos, nomeadamente, sobre a import�ncia do foco nos m�todos direccionados para os utilizadores principais. Entretanto, parece tamb�m ser urgente e fundamental investigar a forma com que as an�lises ergon�micas tem sido aplicadas, assim como, as adapta��es necess�rias a tais m�todos de usabilidade, de modo a definirem-se avalia��es mais coerentes com a natureza do sistema. Sendo assim, com base na observa��o dos sistemas de E-learning - neste artigo ser� apresentada uma revis�o bibliogr�fica quanto �s principais formas de avalia��o de usabilidade em sistemas educativos. Como resultado desta revis�o, os estudos de Ergonomia levam-nos a considerar possibilidades de an�lise da usabilidade atrav�s de um ponto de vista mais humano, onde se equaciona a influ�ncia que o background do utilizador poder� ter sobre a interac��o com o sistema e, consequentemente, que atributos de usabilidade ser�o mais significativos para aquele determinado perfil de utilizador. Neste sentido, o presente estudo pretende argumentar, atrav�s de uma vis�o geral do estado-da-arte, em prol da necessidade e da import�ncia que o investigador deve ter sobre a no��o exacta dos instrumentos de que disp�e, por forma a averiguar os dados que o utilizador poder� fornecer-lhe e qual a relev�ncia dos resultados obtidos para a introdu��o de melhorias no sistema. Ao longo do artigo � efectuada uma discuss�o sobre m�todos qualitativos de avalia��o de usabilidade, baseados em experi�ncias com sistemas de E-learning, acad�micos e/ou comerciais, ao incluir utilizadores com origens em diversos pa�ses e culturas. Dito isto, este artigo pretende retratar uma mudan�a de paradigma de avalia��o que tem sido observada nos �ltimos anos, tanto na �rea de ergonomia, como na �rea do design de sistemas educativos.

2010

abstracts on (turn off)

J. C. Silva, J. C. Campos and J. A. Saraiva (2010)
GUI Inspection from Source Code Analysis. Electronic Communications of the EASST, 33: Foundations and Techniques for Open Source Software Certification 2010).
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.
 

P. Borges, J. Machado, E. Villani and J. C. Campos (2010)
From SFC Specification to C Programming Language on the Context of Aerospace Systems Control. In Ioan Dumitrache and Catalin Buiu, editors, IFAC Workshop on Intelligent Control Systems 2010, pages 46-51. Elsevier. (ISBN: 978-1-61782-758-7)
Aerospace systems software is developed taking into account some precautions to avoid dangerous situations. Usually the controllers of these systems are critical embedded real-time controllers and the respective software programs are developed in the C programming language. This paper is developed on the context of developing embedded critical real-time systems software, for aerospace systems applications, based on formalisms commonly used in the industrial automation field. More precisely, the approach proposed, in this paper, consists in translating a SFC specification to C programming language code considering also the behaviour of the controller device, where the specification will be implemented. An illustrative case study is presented in the end of the paper in order to facilitate the understanding of the proposed approach.

J. L. Silva, O. R. Ribeiro, J. M. Fernandes, J. C. Campos and M. D. Harrison (2010)
The APEX framework: prototyping of ubiquitous environments based on Petri nets. In R. Bernhaupt, P. Forbrig, J. Gulliksen and M.K. L�rusd�ttir, editors, Human-Centred Software Engineering, volume 6409 of Lecture Notes in Computer Science, pages 6-21. Springer.
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This paper reports on an ongoing effort to explore how model-based rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.
 

J. C. Silva, C. E. Silva, J. C. Campos and J. A. Saraiva (2010)
GUI Behavior from Source Code Analysis. In O. Mealha, J. Madeira, D. T�rcio and B.S. Santos, editors, 4a. Confer�ncia Nacional em Interac��o Humano-Computador (Interac��o 2010), pages 81-88. GPCG (Eurographics - Portuguese Chapter).
When developing interactive applications, considering the correctness of graphical user interfaces (GUIs) code is essential. GUIs are critical components of today's software, and contemporary software tools do not provide enough support for ensuring GUIs' code quality. GUIsurfer, a GUI reverse engineering tool, enables evaluation of behavioral properties of user interfaces. It performs static analysis of GUI code, generating state machines that can help in the evaluation of interactive applications. This paper describes the design, software architecture, and the use of GUIsurfer through an example. The tool is easily re-targetable, and support is available to Java/Swing, and WxHaskell. The paper sets the ground for a generalization effort to consider rich internet applications. It explores the GWT web applications' user interface programming toolkit.
 

J.L. Silva, O.R. Ribeiro, J.M. Fernandes, J.C. Campos and M.D. Harrison (2010)
Prototipagem r�pida de ambientes ub�quos. In O. Mealha, J. Madeira, D. T�rcio and B.S. Santos, editors, 4a. Confer�ncia Nacional em Interac��o Humano-Computador (Interac��o 2010), pages 121-128. GPCG (Eurographics - Portuguese Chapter).
A experi�ncia de utiliza��o de ambiente ub�quos � um factor determinante no seu sucesso. As caracter�sticas de tais sistemas devem ser exploradas o mais cedo poss�vel para antecipar potenciais problemas de utiliza��o por parte do utilizador e para reduzir custos de re-design. No entanto, o desenvolvimento antecipado de prot�tipos a serem avaliados no ambiente final pode ser disruptivo e tornar-se inaceit�vel. O desenvolvimento de prot�tipos de ambientes ub�quos pode ajudar, fornecendo indica��es de como o utilizador ir� reagir perante os ambientes. Este artigo descreve o APEX, uma plataforma de prototipagem r�pida de ambientes ub�quos que junta a CPN Tools com um servidor de aplica��es 3D existente. Os prot�tipos desenvolvidos com o APEX permitem que os utilizadores naveguem num mundo virtual, podendo experimentar muitas das caracter�sticas do design proposto. A arquitectura do APEX e a modela��o baseada em CPN s�o descritas. Um exemplo ilustra a abordagem.
 

P. Borges, E. Villani, J. Machado, J. Ferreira and J. Campos (2010)
Abordagem Sistem�tica para o Controlo Seguro de Sistemas aeroespaciais. In XIV International Congress on Project Engineering, pages 2666-2676. FGUPM.
A verifica��o formal do comportamento de sistemas tempo-real � uma tarefa complexa, por v�rias raz�es. H� m�ltiplos trabalhos desenvolvidos na �rea de verifica��o formal, por model-checking de sistemas tempo-real, sendo que diversos softwares foram desenvolvidos para o efeito. Um dos problemas mais complexos para serem resolvidos na an�lise de controladores tempo-real � a convers�o das linguagens de programa��o dos controladores nas linguagens formais, por exemplo aut�matos finitos temporizados para depois poderem ser verificados formalmente atrav�s dos model-checkers existentes. Se a metodologia de elabora��o dos programas for bem desenvolvida e conhecida, essa tarefa pode ser muito facilitada. Por outro lado, grande parte dos sistemas tempo-real (principalmente os sistemas embebidos que pretendemos estudar) � programado em linguagem C. Neste artigo pretende-se estabelecer uma metodologia de cria��o de programas em c�digo C, a partir do formalismo de especifica��o SFC, tendo em conta a verifica��o formal de propriedades comportamentais desejadas para o sistema, utilizando a t�cnica Model-Checking e o model-checker UPPAAL.

J.C. Silva, C. Silva, R. Goncalo, J. Saraiva and J.C. Campos (2010)
The GUISurfer tool: towards a language independent approach to reverse engineering GUI code. In Proceedings of the 2nd ACM SIGCHI Symposium on Engineering interactive computing systems, pages 181-186. ACM. (ISBN: 978-1-4503-0083-4)
Graphical user interfaces (GUIs) are critical components of today's software. Developers are dedicating a larger portion of code to implementing them. Given their increased importance, correctness of GUIs code is becoming essential. This paper describes the latest results in the development of GUISurfer, a tool to reverse engineer the GUI layer of interactive computing systems. The ultimate goal of the tool is to enable analysis of interactive system from source code.
 

M.A. Barbosa, L.S. Barbosa and J.C. Campos (2010)
A coordination model for interactive components. In Fundamentals of Software Engineering, volume 5961 of Lecture Notes in Computer Science, pages 416-430. Springer-Verlag. (ISBN: 978-3-642-11622-3)
Although presented with a variety of 'flavours', the notion of an interactor, as an abstract characterisation of an interactive component, is well-known in the area of formal modelling techniques for interactive systems. This paper replaces traditional, hierarchical, 'tree-like' composition of interactors in the specification of complex interactive systems, by their exogenous coordination through general-purpose software connectors which assure the flow of data and the meet of synchronisation constraints. The paper's technical contribution is twofold. First a modal logic is defined to express behavioural properties of both interactors and connectors. The logic is new in the sense that its modalities are indexed by sets of actions to cater for action co-occurrence. Then, this logic is used in the specification of both interactors and coordination layers which orchestrate their interconnection.
 

L. Freire, P.M. Arezes and J.C. Campos (2010)
Princ�pios de Ergonomia e Design discutidos atrav�s de plataformas utilizadas para e-learning. In P. Arezes, J.S. Baptista, M.P. Barroso, P. Carneiro, P. Cordeiro, N. Costa, R. Melo, A.S. Miguel and G.P. Perestrelo, editors, Occupational Safety and Hygiene (SHO 2010), pages 256-260. (ISBN: 978-972-99504-6-9)
O presente artigo tem como objectivo principal apresentar uma revis�o bibliogr�fica referente aos princ�pios de Ergonomia aplicados a ferramentas utilizadas para e-learning. � sabido que os erros na aplica��o destes princ�pios acarretam sobrecargas cognitivas nos utilizadores destas plataformas, pelo que o artigo procura abordar o tema de forma abrangente. Deste modo, na primeira parte deste artigo apresentam-se os princ�pios ergon�micos mais referenciados como fundamentos de Ergonomia Cognitiva e Informacional e, em seguida, apresentam-se as directrizes de usabilidade destinadas a sistemas de informa��o que poder�o servir como suporte para interac��es acad�micas. Na segunda parte, realiza-se um discuss�o acerca de uma observa��o de experi�ncias de aprendizagem colaborativa vivenciadas entre professores e alunos em projectos de pesquisa e extens�o. A metodologia deste artigo aponta para uma estrutura de investiga��o de natureza qualitativa, onde o objectivo era perceber as interac��es vividas virtualmente, enquanto utilizadores de sistemas cuja meta � favorecer a constru��o de conhecimentos de car�cter acad�mico. Os resultados desta investiga��o configuram-se como uma forma adicional de an�lise das quest�es referentes � Ergonomia, de modo a que os sistemas informacionais privilegiem sempre os diferentes perfis dos seus utilizadores.

2009

abstracts on (turn off)

J. C. Campos and J. Machado (2009)
Pattern-based Analysis of Automated Production Systems. IFAC Proceedings Volumes, 42(4):972-977.
As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics in which properties are expressed is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of security if gained with the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. This paper illustrates how a collection of property patterns, and its tool support, can help in simplifying the process of generating logical formulae from informally expressed requirements.
 

J. C. Campos and S. Mendes (2009)
FlexiXML: Um animador de modelos UsiXML. In 17o. Encontro Portugu�s de Computa��o Gr�fica (17o. EPCG), pages 185-194. GPCG (Eurographics - Portuguese Chapter). (ISBN: 978-972-98464-3-4)
Uma parte consider�vel do desenvolvimento de software � dedicada � camada de interac��o com o utilizador. Face � complexidade inerente ao desenvolvimento desta camada, � importante possibilitar uma an�lise t�o cedo quanto poss�vel dos conceitos e ideias em desenvolvimento para uma dada interface. O desenvolvimento baseado em modelos fornece uma solu��o para este problema ao facilitar a prototipagem de interfaces a partir dos modelos desenvolvidos. Este artigo descreve uma abordagem � prototipagem de interfaces e apresenta a primeira vers�o da ferramenta FlexiXML que realiza a interpreta��o e anima��o de interfaces descritas em UsiXML.
 

R. Paulo, A. Carrapatoso, M. Lemos, R. Bernardo and J. Campos (2009)
Advanced Engineering Tools for Next Generation Substation Automation Systems: The Added Value of IEC 61850 and the InPACT Project. In 20th International Conference and Exhibition on Electricity Distribution (CIRED 2009), volume PEP0550Z of IET Conference Publications, pages 0322/1-4. IET. (ISSN: 0537-9989, ISBN: 978-1-84919-126-5)
Automation systems according to IEC 61850 are a powerful solution for station automation. Engineering of such distributed systems is however a non-trivial task which requires different approaches and enhanced tool support. In this paper the authors (i) present how IEC 61850 is viewed and is being adopted by a utility and vendor, (ii) discuss its engineering potential and current issues, (iii) point-out global requirements for next generation tools, (iv)present the InPACTproject which is tackling some of these concerns and (v) propose key elements of visual languages as one contributing enhancement.
 

J. C. Campos and M. D. Harrison (2009)
Interaction engineering using the IVY tool. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pages 35-44. ACM.
This paper is concerned with support for the process of usability engineering. The aim is to use formal techniques to provide a systematic approach that is more traceable, and because it is systematic, repeatable. As a result of this systematic process some of the more subjective aspects of the analysis can be removed. The technique explores exhaustively those features of a specific design that fail to satisfy a set of properties. It also analyzes those aspects of the design where it is possible to quantify the cost of use. The method is illustrated using the example of a medical device. While many aspects of the approach and its tool support have already been discussed elsewhere, this paper builds on and contrasts an analysis of the same device provided by a third party and in so doing enhances the IVY tool.
   

J. L. Silva, J. C. Campos and M. D. Harrison (2009)
An infrastructure for experience centered agile prototyping of ambient intelligence. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pages 79-84. ACM.
Ubiquitous computing poses new usability challenges that cut across design and development. We are particularly interested in "spaces" enhanced with sensors, public displays and personal devices. How can prototypes be used to explore the user's mobility and interaction, both explicitly and implicitly, to access services within these environments? Because of the potential cost of development and design failure, the characteristics of such systems must be explored using early versions of the system that could disrupt if used in the target environment. Being able to evaluate these systems early in the process is crucial to their successful development. This paper reports on an effort to develop a framework for the rapid prototyping and analysis of ambient intelligence systems.
   

J.C. Silva, J. Saraiva and J.C. Campos (2009)
A Generic Library for GUI Reasoning and Testing. In SAC '09: Proceedings of the 2009 ACM Symposium on Applied Computing, pages 121-128. ACM. (ISBN: 978-1-60558-166-8)
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 presents a generic model for language-independent reverse engineering of graphical user interface based applications, and we explore the integration of model-based testing techniques in our approach, thus allowing us to perform fault detection. A prototype tool has been constructed, which is already capable of deriving and testing a user interface behavioral model of applications written in Java/Swing.
 

2008

abstracts on (turn off)

J.C. Campos and M.D. Harrison (2008)
Considering context and users in interactive systems analysis. In Engineering Interactive Systems, volume 4940 of Lecture Notes in Computer Science, pages 193-209. Springer-Verlag. (ISBN: 978-3-540-92697-9)

M. Harrison and J. C. Campos (2008)
Analysing Human Aspects of Safety-Critical Software. ERCIM News, 75:18, October. (Invited paper; ISSN: 0926-4981)
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.
 

M. D. Harrison, J. C. Campos and K. Loer (2008)
Formal analysis of interactive systems: opportunities and weaknesses. In P. Cairns and A. Cox, editors, Research Methods in Human Computer Interaction, chapter 5, pages 88-111. Cambridge University Press.
Although formal techniques are not widely used in the analysis of interactive systems there are reasons why an appropriate set of tools, suitably designed to be usable by system engineers, could be of value in the portfolio of techniques used to assess interactive systems. This chapter describes the role of formal techniques in modelling and analysing interactive systems, discusses unfulfilled opportunities and speculates about the removal of barriers to their use. It also presents the opportunities that a clear expression of the problem and systematic analysis techniques may afford.
 

J. C. Campos, Daniel Gon�alves, T. Rom�o and L. Rato, editor(s) (2008)
Interac��o 2008 - Actas da 3a. Confer�ncia Nacional em Interac��o Pessoa-M�quina. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-9-9)

N. Guerreiro, S. Mendes, V. Pinheiro and J. C. Campos (2008)
AniMAL - a user interface prototyper and animator for MAL interactor models. In J.C. Campos, D. Gon�alves, T. Rom�o and L. Rato, editors, Interac��o 2008 - Actas da 3a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 93-102. Grupo Portugu�s de Computa��o Gr�fica.
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.

M. Borges, J. C. Campos and A. N. Ribeiro (2008)
Framework de distribui��o ass�ncrona de aplica��es m�veis situadas. In J.C. Campos, D. Gon�alves, T. Rom�o and L. Rato, editors, Interac��o 2008 - Actas da 3a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 181-186. Grupo Portugu�s de Computa��o Gr�fica.

J. C. Campos, J. Machado and E. Seabra (2008)
Property Patterns for the Formal Verification of Automated Production Systems. In Proceedings of the 17th IFAC World Congress, pages 5107-5112. IFAC.
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.
 

J. C. Campos and M. D. Harrison (2008)
Systematic analysis of control panel interfaces using formal tools. In XVth International Workshop on the Design, Verification and Specification of Interactive Systems (DSV-IS 2008), number 5136 of Lecture Notes in Computer Science, pages 72-85. Springer-Verlag.
   

G. J. Doherty, J. C. Campos and M. D. Harrison (2008)
Resources for Situated Actions. In XVth International Workshop on the Design, Verification and Specification of Interactive Systems (DSV-IS 2008), number 5136 of Lecture Notes in Computer Science, pages 194-207. Springer-Verlag.
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.
   

M. D. Harrison, J. C. Campos, G. Doherty and K. Loer (2008)
Connecting rigorous system analysis to experience centred design. In E. Law, E. Hvannberg and G. Cockton, editors, Maturing Usability: Quality in Software, Interaction and Value, Human-Computer Interaction Series, chapter 3, pages 56-74. Springer. (ISSN: 1571-5035; ISBN: 978-1-84628-940-8)
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 require- ments 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 relat- ing 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.
 

J. L. Silva, J. C. Campos and A. Paiva (2008)
Model-based user interface testing with Spec Explorer and ConcurTaskTrees. Electronic Notes in Theoretical Computer Science, 208:77-93.
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.
 

M. Harrison, C. Kray and J. C. Campos (2008)
Exploring an option space to engineer a ubiquitous computing system. Electronic Notes in Theoretical Computer Science, 208:41-55.
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.
 

2007

abstracts on (turn off)

J. Machado, E. Seabra, J.C. Campos, F. Soares, C.P. Leao and J.F. Silva (2007)
Simulation and Formal Verification of Industrial Systems Controllers. In 19th International Congress of Mechanical Engineering (COBEM 2007). ABCM. (ISBN: 978-85-85769-34-5)

J. Machado, E. Seabra, F. Soares and J. Campos (2007)
A New Plant Modelling Approach For Formal Verification Purposes. IFAC Proceedings Volumes, 40(9):167-172.
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
 

H. Pinto, R. Jos� and J. C. Campos (2007)
An Interaction Model and Infrastructure for Localized Activities in Pervasive Computing Environments. In IEEE International Conference on Pervasive Services 2007 (ICPS'07), pages 232-241. IEEE Computer Society Press. (ar: 18/64 ~.28)
   

A. N. Ribeiro, J. C. Campos and F. Martins (2007)
Integrating HCI into a UML based Software Engineering course. In Proceedings HCI Educators 2007, pages 48-57. GPCG (Eurographics - Portuguese Chapter).
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 de- sign 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 designs, 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

S. Chatty, J. C. Campos, M. P. Gonzalez, S. Lepreux, E. G. Nilsson, V. Penichet and M. Santos J. Van den Bergh (2007)
Processes: Working group report. In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, volume 4323 of Lecture Notes in Computer Science, pages 262-264. Springer-Verlag.
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.
 

J. C. Silva, J. C. Campos and J. Saraiva (2007)
Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications. In G. Doherty and A. Blandford, editors, Interactive Systems: Design, Specification and Verification, volume 4323 of Lecture Notes in Computer Science, pages 137-150. Springer-Verlag.
   

M. A. Barbosa, L. S. Barbosa and J. C. Campos (2007)
Towards a coordination model for interactive systems. Electronic Notes in Theorectical Computer Science, 183:73-88.
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.
   

2006

abstracts on (turn off)

T. Chambel, N. J. Nunes, T. Rom�o and J. C. Campos, editor(s) (2006)
Interac��o 2006 - Actas da 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-7-2)
A concep��o e desenvolvimento de sistemas interactivos envolve aspectos que v�o desde a psicologia � engenharia de software. Recentemente verificou-se uma r�pida evolu��o nesta �rea multidisciplinar, tanto a n�vel tecnol�gico, como do contexto de utiliza��o da tecnologia. Assim, �s tradicionais preocupa��es com a efic�cia, efici�ncia e satisfa��o, juntam-se agora quest�es como entretenimento, design, est�tica, coopera��o, ubiquidade e adaptabilidade. Paralelamente, o leque de utilizadores alvo dos sistemas � cada vez mais alargado, existindo a preocupa��o de desensenvolver interfaces para pessoas e contextos de utiliza��o com diferentes tipos de necessidades e requisitos ao n�vel f�sico ou cognitivo. Torna-se assim necess�rio perceber o impacto destas novas realidades no processo de interac��o e no desenvolvimento de sistemas interactivos.

Depois do sucesso da primeira edi��o, organizada em Julho de 2004 na Faculdade de Ci�ncia da Universidade de Lisboa, organizou-se agora a Interac��o 2006 -- 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina -- numa iniciativa conjunta do Grupo Portugu�s de Computa��o Gr�fica e do Departamento de Inform�tica/Centro de Ci�ncias da Computa��o da Universidade do Minho. Tal como na sua primeira edi��o, a Interac��o 2006 visou promover um ponto de encontro da comunidade interessada na Interac��o Pessoa-M�quina em Portugal. Reunindo investigadores, docentes e profissionais, permitiu a divulga��o de trabalhos e a troca de experi�ncias entre as comunidades acad�mica e industrial.

Adoptando uma postura marcadamente multidisciplinar, a confer�ncia desafiou os autores a abordar desde os fundamentos te�ricos �s pr�ticas e aplica��es emergentes, visando explorar sinergias nas seguintes dimens�es:

• Aspectos Te�ricos em Interac��o Pessoa-M�quina
• Concep��o, Desenvolvimento e Avalia��o de Sistemas Interactivos
• Tecnologias de Suporte � Interac��o
• Aplica��es Interactivas

Em resposta a este desafio, foram recebidos trabalhos de Portugal, Espanha e Brasil.

Como resultado do processo de revis�o dos trabalhos propostos, foram organizadas sete sess�es t�cnicas em que foram apresentados 13 artigos longos e 16 artigos curtos, bem como uma sess�o de posters e demonstra��es em que foram apresentados 9 trabalhos. Para complementar o programa t�cnico foram ainda organizadas duas sess�es proferidas por convidados internacionais de renome e uma sess�o dedicada � ind�stria, em que se convidaram empresas e uma associa��o a apresentar a sua perspectiva sobre o tema da Usabilidade.

A confer�ncia decorreu entre os dias 16 e 18 de Outubro de 2006, nas instala��es da Universidade do Minho, Campus de Gualtar, em Braga. Procurou-se que ela fosse um retrato do trabalho que vem sendo desenvolvido nesta �rea em Portugal. Assim, as sess�es t�cnicas desenvolveram-se em torno de sete temas principais, seleccionados a partir da an�lise dos trabalhos aceites: Acessibilidade, Psicologia Cognitiva e Colabora��o, Concep��o e Desenvolvimento, Interfaces Multimodais e Adaptativas, Realidade Virtual e Aumentada, Vizualiza��o e Pesquisa de Informa��o, e Avalia��o. Sem se tratar de uma classifica��o estanque, pensamos ser esta uma organiza��o natural e abrangente dos trabalhos apresentados.

Terminamos agradecendo aos membros do Comit� Organizador e da Comiss�o de Programa todo o seu trabalho, aos oradores convidados, Michael D. Harrison e Larry L. Constantine, bem como �s institu��es que aceitaram o desafio de participar na sess�o dedicada � ind�stria (Associa��o Portuguesa de Profissionais de Usabilidade, MobiComp, Wintouch e Edigma.com) e a todos os autores. Agradecemos finalmente a todos os patrocinadores por nos ajudarem a tornar este evento poss�vel. Esperamos que esta tenha sido mais uma contribui��o para fomentar a partilha e colabora��o da comunidade Interac��o Pessoa-M�quina em Portugal.

J. C. Campos and G. J. Doherty (2006)
Supporting resource-based analysis of task information needs. In S.W. Gilroy and M.D. Harrison, editors, Interactive Systems: Design, Specification and Verification, volume 3941 of Lecture Notes in Computer Science, pages 188-200. Springer-Verlag. (ISSN: 0302-9743, ISBN: 3-540-34145-5)
   

J. C. Campos and M. D. Harrison (2006)
Automated deduction and usability reasoning. In Claude Ghaoui, editor, Encyclopedia of Human-Computer Interaction, pages 45-54. Idea Group Reference. (ISBN: 1-59140-562-9 - hardcover / 1-59140-798-2 - ebook)
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.

J. C. Campos and A. N. Ribeiro (2006)
UML no Desenvolvimento de Sistemas Interactivos. In T. Chambel, N. J. Nunes, T. Rom�o and J. C. Campos, editors, Interac��o 2006 - Actas da 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 77-80. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-7-2)
 

A. R. Fernandes, J. R. Pereira and J. C. Campos (2006)
Accessibility and Visually Impaired Users. In I. Seruca, J. Filipe, S. Hammoudi and J. Cordeiro, editors, Enterprise Information Systems VI. Springer. (ISBN: 1-4020-3674-4). (Best papers from ICEIS 2005 - ar (ICEIS 2005): .19)
Internet accessibility for the visually impaired community is still an open issue. Guidelines have been issued by the W3C consortium to help web designers to improve web site accessibility. However several studies show that a significant percentage of web page creators are still ignoring the proposed guidelines. Several tools are now available, general purpose, or web specific, to help visually impaired readers. But is reading a web page enough? Regular sighted users are able to scan a web page for a particular piece of information at high speeds. Shouldn't visually impaired readers have the same chance? This paper discusses some features already implemented to improve accessibility and presents a user feedback report regarding the AudioBrowser, a talking browser. Based on the user feedback the paper also suggests some avenues for future work in order to make talking browsers and screen readers compatible.
 

A. Mano and J. C. Campos (2006)
Usabilidade em interfaces para crian�as. Jornal de Ci�ncias Cognitivas, Setembro. (ISSN: 1646-365X)
 

A. Mano and J. C. Campos (2006)
Cognitive walkthroughs in the evaluation of user interfaces for children. In T. Chambel, N. J. Nunes, T. Rom�o and J. C. Campos, editors, Interac��o 2006 - Actas da 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 195-198. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-7-2)

M. Borges, A. N. Ribeiro and J. C. Campos (2006)
A Push Infrastructure for Mobile Application Deployment in Mobile Environments. In R. Jos� and C. Baquero, editors, CSMU 2006 -- Conference on Mobile and Ubiquitous Systems, pages 175-178. Escola de Engenharia, Universidade do Minho. (ISBN: 972-8692-29-3)
Mobile devices tend to be a synonym of variety. Variety both in hardware capabilities and software act as restrictions to software development and deployment. Other restrictions arise from their condition of mobility, environmental conditions such as bandwidth, coverage availability, lighting and availability of services. In that perspective, this work intends to explore the possibility of a model of application deployment and execution that minimizes these issues - software gets pushed through an infrastructure and interaction between the user and the application is expected to have a behaviour between these two modes: purely client based and purely online based.

S. Rodrigues, J. C. Campos and A. N. Ribeiro (2006)
Adapta��o nativa de interfaces com o utilizador em dispositivos m�veis. In CSMU 2006 - Conference on Mobile and Ubiquitous Systems, pages 171-174. Escola de Engenharia, Universidade do Minho. (ISBN: 972-8692-29-3)
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.

J. C. Silva, J. C. Campos and J. Saraiva (2006)
Models for the Reverse Engineering of Java/Swing Applications. In J. M. Favre, D. Gasevic, R. L�mmel and A. Winter, editors, 3rd International Workshop on Metamodels, Schemas, Grammars, and Ontologies (ateM 2006) for Reverse Engineering, number 1/2006 of Informatik-Bericht series. Johannes Gutenberg-Universit�t Mainz, Institut f�ur Informatik - FB 8. (ISSN: 0931-9972)
   

J. C. Silva, J. C. Campos and J. Saraiva (2006)
Engenharia Reversa de Sistemas Interactivos Desenvolvidos em Java2/Swing. In T. Chambel, N. J. Nunes, T. Rom�o and J. C. Campos, editors, Interac��o 2006 - Actas da 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 63-72. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-7-2)
 

N. M. E. Sousa and J. C. Campos (2006)
IVY Trace Visualiser. In T. Chambel, N. J. Nunes, T. Rom�o and J. C. Campos, editors, Interac��o 2006 - Actas da 2a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 181-190. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-7-2)
 

2005

abstracts on (turn off)

J. C. Campos (2005)
Model based web interfaces' analysis. In HCI International 2005 - 11th International Conference on Human-Computer Interaction (posters section). Laurence Erlbaum Associates, Inc. (ISBN: 0-8085-5807-5 - CD-ROM edition)

J. C. Campos and A. R. Fernandes (2005)
Testing AudioBrowser. In HCI International - 11th International Conference on Human-Computer Interaction (posters section). Laurence Erlbaum Associates, Inc.. (ISBN: 0-8085-5807-5 - CD-ROM edition)

M.Harrison, G. Doherty and J. C. Campos (2005)
Is there a role for rigorous system analysis in experience centred design?. Position paper for the Workshop on Space, Place, and Experience in Human Computer Interaction, 10th IFIP International Conference on Human Computer Interaction -- Interact 2005. September.

A. Mano and J. C. Campos (2005)
A study on usability criteria regarding interfaces for children. In Interact 2005 Workshop on Child Computer Interaction: Methodological Research, pages 32-35.
 

L. Teixeira, �. Costa, V. Pereira, C. P. Le�o, F. O. Soares, M. T. Restivo, F. Chouzal, J. Mendes and J. C. Campos (2005)
Laborat�rios virtuais: duas aplica��es no ensino de engenharia. In A. Mendes, I. Pereira and R. Costa, editors, VII Simp�sio Internacional de Inform�tica Educativa -- SIIE'05 (posters section). (ISBN: 972-95207-4-7 (CD-ROM edition))

2004

abstracts on (turn off)

J. C. Campos (2004)
Interactors as Boundary Objects. Position paper at the CHI 2004 workshop: Identifying Gaps between HCI, Software Engineering, and Design, and Boundary Objects to Bridge Them. April.

J. C. Campos (2004)
The modelling gap between software engineering and human-computer interaction. In Rick Kazman, Len Bass and Bonnie John, editors, ICSE 2004 Workshop: Bridging the Gaps II, pages 54-61. The IEE. (ISBN: 0-86341-416-8)
The theories and practices of software engineering and of human-computer interaction have, to a great extent, evolved separately. It seems obvious that the development of an interactive system would benefit from input from both disciplines. In practice, however, the communication between the two communities has been difficult. Models can be a particularly good tool for communication. For that to happen the differences between the models used by each community must first be identified and understood. This paper looks at the gaps between the models used by the software engineering and the human-computer interaction communities. It identifies where differences between these models can be found, and some aspects that need addressing in order to promote better communication.
 

J. C. Campos (2004)
An�lise de usabilidade baseada em modelos. In Intera��o 2004 - 1a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 171-176. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-4-8 (proceedings also available as a special number of the {Virtual} electronic journal, ISSN: 0873-1837))
A norma ISO DIS 9241-11 define usabilidade de um sistema como a efic�cia, efici�ncia e satisfa��o com que utilizadores determinados atingem objectivos determinados em ambientes espec�ficos. A an�lise de usabilidade de um sistema deve ent�o ter em considera��o os utilizadores e o contexto de utiliza��o. Isto coloca problemas pois tipicamente os engenheiros de software n�o est�o motivados, nem tem os conhecimentos necess�rios, para analisarem o sistema desta perspectiva. Neste artigo apresenta-se a arquitectura de uma ferramenta que suporta uma abordagem ao desenvolvimento de sistemas interactivos em que se procura facilitar a comunica��o entre as comunidades da Interac��o Humano-Computador e da Engenharia de Software.

J. C. Campos, M. D. Harrison and Karsten Loer (2004)
Verifying user interface behaviour with model checking. In J. C. Augusto and U. Ultes-Nitsche, editors, Verification and Validation of Enterprise Information Systems (VVEIS 2004), pages 87-96. INSTICC Press. (ISBN: 972-8865-03-1)
 

A. R. Fernandes, J. R. Pereira and J. C. Campos (2004)
Accessibility and Visually Impaired Users. In I. Seruca, J. Filipe, S. Hammoudi and J. Cordeiro, editors, ICEIS 2004: Proceedings of the 6th International Conference on Enterprise Information Systems, volume 5, pages 75-80. INSTICC Press. (ISBN: 972-8865-00-7)
Internet accessibility for the visually impaired community is still an open issue. Guidelines have been issued by the W3C consortium to help web designers to improve web site accessibility. However several studies show that a significant percentage of web page creators are still ignoring the proposed guidelines. Several tools are now available, general purpose, or web specific, to help visually impaired readers. But is reading a web page enough? Regular sighted users are able to scan a web page for a particular piece of information at high speeds. Shouldn't visually impaired readers have the same chance? This paper discusses some features already implemented to improve accessibility and presents a user feedback report regarding the AudioBrowser, a talking browser. Based on the user feedback the paper also suggests some avenues for future work in order to make talking browsers and screen readers compatible.

A. Mano and J. C. Campos (2004)
A study about usability criteria on computer interfaces for children. In First Portuguese Forum of Experimental Psychology.
This study's main goal is to produce a set of guidelines intended to aid a programmer who wishes to build a computer application targeted at children ranging from 5 to 7 years old.

A. Mano and J. C. Campos (2004)
Aplica��o de um Cognitive Walkthrough - estudo de caso. In Intera��o 2004 - 1a. Confer�ncia Nacional em Interac��o Pessoa-M�quina, pages 256-258. Grupo Portugu�s de Computa��o Gr�fica. (ISBN: 972-98464-4-8 (proceedings also available as a special number of the {Virtual} electronic journal, ISSN: 0873-1837))
Esta comunica��o � uma tentativa de sistematizar a aplica��o de um m�todo de an�lise de usabilidade: o cognitive walkthrough. Pode ent�o ser utilizada como um tutorial, apresentando um exemplo da aplica��o do m�todo a uma situa��o pr�tica.

2003

abstracts on (turn off)

J. C. Campos (2003)
Using task knowledge to guide interactor specifications analysis. In J. A. Jorge, N. J. Nunes and J. Falcão e Cunha, editors, Interactive Systems: Design, Specification and Verification, volume 2844 of Lecture Notes in Computer Science, pages 171-186. Springer-Verlag. (ISSN: 0302-9743, ISBN: 3-540-20159-9)
   

J. C. Campos (2003)
Uma abordagem formal � Engenharia da Usabilidade. In Simone D. J. Barbosa and Cleotilde Gonzalez, editors, CLIHC 2003 Conference Proceedings, ACM International Conference Proceeding Series, pages 17-28. ACM. (ISBN: 85-87926-05-5)
The quality of an interactive system can be measured in terms of its usability. Empirical approaches to usability evaluation attempt to assess the system under real usage conditions. This type of approach can be very expensive. Analytical approaches have been proposed as a means of reasoning about usability issues from early in development. These approaches use models to focus the analysis in specific usability issues. In this context, the application of (mathematically) formal notations and tools has been proposed. This paper presents a formal approach to the analysis of interactive systems. The analysis can be carried out taking into account all possible behaviours of the device, or it can be guided by the tasks the device is supposed to support.
 

J. C. Campos and G. J. Doherty (2003)
Reasoning about Dynamic Information Displays. In J. A. Jorge, N. J. Nunes and J. Falc�o e Cunha, editors, Interactive Systems: Design, Specification and Verification, volume 2844 of Lecture Notes in Computer Science, pages 288-302. Springer-Verlag. (ISSN: 0302-9743, ISBN: 3-540-20159-9)
 

J. C. Campos and M. D. Harrison (2003)
From HCI to Software Engineering and back. In Rick Kazman, Len Bass and Jan Bosch, editors, Bridging the Gaps Between Software Engineering and Human-Computer Interaction, ICSE '2003 workshop, pages 49-56.
 

2001

abstracts on (turn off)

J. C. Campos and G. J. Doherty (2001)
Reasoning about Time in Dynamic Information Displays. In G.J. Doherty, M. Massink and M.D. Wilson, editors, Continuity in Future Computing Systems - Proceedings of I³ Spring Days Workshop, volume RAL-CONF-2001-001 of RAL Conference Proceedings, pages 80-95. Council for the Central Laboratory of the Research Councils. (ISSN: 1362-0231)
With increasing use of computing systems while on the move and in constantly changing conditions, whether it is via mobile devices, wearable computers or embedded systems in the environment, time plays an increasingly important role in interaction. The way in which information is represented in an interface is fundamental to interaction with it, and how we use the information in the users tasks and activities. Dynamic representations where the user must perceive changes in the information displayed over time pose a further challenge to the designer. The diminutive size and limited display capabilities of many ubiquitous computing devices further motivate careful design of these displays. In this paper we look at how time can be taken into account when reasoning about representational issues from the early stages of design. We look at a model which can be used to reason about these issues in a structured fashion, and apply it to an example.
 

J. C. Campos and M. D. Harrison (2001)
Model Checking Interactor Specifications. Automated Software Engineering, 8(3):275-310, August. (ISSN: 0928-8910)
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 {\em 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 {\em 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.
   

2000

abstracts on (turn off)

G. J. Doherty, J. C. Campos and M. D. Harrison (2000)
Representational Reasoning and Verification. Formal Aspects of Computing, 12(4):260-277. (ISSN: 0934-5043)
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.
   

1999

abstracts on (turn off)

J. C. Campos (1999)
Automated Deduction and Usability Reasoning. DPhil thesis, Department of Computer Science, University of York. (Also available as Technical Report YCST 2000/9, Department of Computer Science, University of York)
 

J. C. Campos and M. D. Harrison (1999)
Using automated reasoning in the design of an audio-visual communication system. In D. J. Duke and A. Puerta, editors, Design, Specification and Verification of Interactive Systems '99, Springer Computer Science, pages 167-188. Springer-Verlag/Wien. (ISSN: 0946-2767, ISBN: 3-211-83405-2)
 

J. C. Campos and M. D. Harrison (1999)
From Interactors to SMV: A Case Study in the Automated Analysis of Interactive Systems. Technical Report YCS-99-317, Department of Computer Science, University of York.
 

1998

abstracts on (turn off)

J. C. Campos (1998)
Integrating Automated Verification into Interactive Systems Development. In 13th IEEE International Conference: Automated Software Engineering - Doctoral Symposium Proceedings, pages 13-15.
Our field of research is the application of automated reasoning techniques during interactor based interactive systems development. The aim being to ensure that the developed systems embody appropriate properties and principles. In this report we identify some of the pitfalls of current approaches and propose a new way to integrate verification into interactive systems development.
 

J. C. Campos and M. D. Harrison (1998)
The role of verification in interactive systems design. In P. Markopoulos and P. Johnson, editors, Design, Specification and Verification of Interactive Systems '98, Springer Computer Science, pages 155-170. Springer-Verlag/Wien. (ISSN: 0946-2767, ISBN: 3-211-83212-2)
 

G. Doherty, J. C. Campos and M. D. Harrison (1998)
Representational Reasoning and Verification. In J. I. Siddiqi, editor, Proceedings of the BCS-FACS Workshop: Formal Aspects of the Human Computer Interaction, pages 193-212. SHU Press. (ISBN: 0-86339-7948)

1997

abstracts on (turn off)

J. C. Campos and M. D. Harrison (1997)
Formally Verifying Interactive Systems: A Review. In M. D. Harrison and J. C. Torres, editors, Design, Specification and Verification of Interactive Systems '97, Springer Computer Science, pages 109-124. Springer-Verlag/Wien. (ISSN: 0946-2767, ISBN: 3-211-83055-3)
 

1996

abstracts on (turn off)

J. C. Campos and F. M. Martins (1996)
Context Sensitive User Interfaces. In C. R. Roast and J. I. Siddiqi, editors, Formal Aspects of the Human Computer Interface, electronic Workshops in Computing. Springer-Verlag London. (ISBN: 3-540-76105-5)
This paper presents a conceptual design model for user interfaces (MASS1) and a general formalism for dialogue specification (Interaction Scripts) which are the most important components of an approach to the methodological, iterative design of Interactive Systems from formal, model-based specification of both the application and the User Interface (UI). This approach allows the integration of both dialogue and application semantics from the beginning of the design process, by using prototypes derived from both specifications. Assuming that all the application semantics is available at early design stages, the MASS model defines a set of guidelines that will enforce the designer to create user interfaces that will present a prophylactic instead of the usual therapeutic behaviour. By a prophylactic behaviour it is meant, metaphorically, that the UI will exhibit a behaviour that prevents and avoids both syntactic and semantic user errors, in contrast with the most usual therapeutic, or error recovery, behaviour. The dialogue specification formalism(Interaction Scripts) despite being general, in the sense that it may be applied to the specification of any kind of dialogue, is specially suited to the specification of UIs with the behaviour prescribed by the MASS design model. In addition, it is independent from concrete environment details, therefore allowing for different implementations of the same specification, that is, different looks and feels. The operational semantics of the Interaction Script notation is also presented in terms of Petri-Nets that are automatically generated from the Interaction Script specification of the dialogue controller.
 

1994

abstracts on (turn off)

J. C. Campos and F. M. Martins (1994)
O Sistema GAMA - Arquitectura e Implementa��o. In F. M. Martins, J. J. Almeida and J. G. Rocha, editors, 6o. Encontro Portugu�s de Computa��o Gr�fica, number UMDIAR9414, pages 2-15.
 

1993

abstracts on (turn off)

J. C. Campos (1993)
GAMA-X Gera��o Semi-Autom�tica de Interfaces Sens�veis ao Contexto. MSc. thesis, Departamento de Inform�tica, Universidade do Minho.

J. C. Campos and F. M. Martins (1993)
GAMA-X - Uma Arquitectura Software para o Desenvolvimento Semi-Autom�tico de Interfaces Utilizador-Sistema. In 5o. Encontro Portugu�s de Computa��o Gr�fica, number UMDIAR9310, pages 197-209.

1991

abstracts on (turn off)

J. C. Campos (1991)
IAPF - Interfaces Assistidas para Prot�tipos Funcionais. Relat�rio de Est�gio, Departamento de Inform�tica, Universidade do Minho.

Generated by mkBiblio 2.6.27