Publications

Borges P, Villani E, Machado J, Campos JC, F. J.  2010.  Abordagem Sistemática para o Controlo Seguro de Sistemas aeroespaciais. XIV International Congress on Project Engineering. :10p. Abstractciip10_2666_2676.2958.pdf

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.

Silva JC, Silva CE, Gonçalo R, Saraiva JA, Campos JC.  2010.  The GUISurfer tool: towards a language independent approach to reverse engineering GUI code. Proceedings of the 2nd ACM SIGCHI Symposium on Engineering interactive computing systems. :181-186. Abstracteics141-silva.pdf

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.

Freire L, Arezes P, Campos JC.  2010.  Princípios de Ergonomia e Design discutidos através de plataformas utilizadas para e-learning. Occupational Safety and Hygiene (SHO 2010). :256-260. Abstractfreireac2010.pdf

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.

Campos JC, Machado J.  2009.  Pattern-based Analysis of Automated Production Systems. 13th IFAC Symposium on Information Control Problems in Manufacturing (INCOM 2009). :972-977. Abstractcamposm2009.pdf

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.

Campos JC, Mendes S.  2009.  FlexiXML: Um animador de modelos UsiXML. 17º Encontro Português de Computação Gráfica - EPCG. :185-194. Abstractcamposm09.pdf

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.

Paulo R, Carrapatoso A, Lemos M, Bernardo R, Campos JC.  2009.  Advanced Engineering Tools for Next Generation Substation Automation Systems: The Added Value of IEC 61850 and the InPACT Project. 20th International Conference and Exhibition on Electricity Distribution - CIRED. PEP0550Z:0322/1-4. Abstractpauloclbc09.pdf

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.

Campos JC, Harrison M.  2009.  Interaction engineering using the IVY tool. ACM Symposium on Engineering Interactive Computing Systems - EICS. :35-44. Abstracteics141-campos.pdf

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.

Silva JL, Campos JC, Harrison M.  2009.  An infrastructure for experience centered agile prototyping of ambient intelligence. ACM Symposium on Engineering Interactive Computing Systems (EICS 2009). :79-84. Abstracteics131-silva.pdf

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.

Silva JC, Saraiva JA, Campos JC.  2009.  A Generic Library for GUI Reasoning and Testing. SAC - Proceedings of the ACM Symposium on Applied Computing. :121-128. Abstract2009-sachci-final.pdf

Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI's code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper 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.

Campos JC, Barbosa LS, Barbosa M.  2009.  A coordination model for interactive components. 3rd International Conference on Fundamentals of Software Engineering - FSEN. Abstractbbc09.pdf

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 fragments of 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.

Campos JC, Harrison M.  2008.  Considering context and users in interactive systems analysis. 2nd Conference on Human-Centred Software Engineering - HCSE and 7th International Workshop on Task Models and Diagrams - TAMODIA. 4940:193-209. Abstracteis07contextvlncs.pdf

Although the take-up of formal approaches to modelling and reasoning about software has been slow, there has been recent interest and facility in the use of automated reasoning techniques such as model checking [5] on increasingly complex systems. In the case of interactive systems, formal methods can be particularly useful in reasoning about systems that involve complex interactions. These techniques for the analysis of interactive systems typically focus on the device and leave the context of use undocumented. In this paper we look at models that incorporate complexity explicitly, and discuss how they can be used in a formal setting. The paper is concerned particularly with the type of analysis that can be performed with them.

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

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

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

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

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

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

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

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