Publications

Riché TL, Gonçalves RC, Marker B, Batory D.  2012.  Pushouts in Software Architecture Design. GPCE '12: Proceedings of the 11th International Conference on Generative Programming and Component Engineering. :84–92. Abstractriche-2012.pdf

A classical approach to program derivation is to progressively extend a simple specification and then incrementally refine it to an implementation. We claim this approach is hard or impractical when reverse engineering legacy software architectures. We present a case study that shows optimizations and pushouts—in addition to refinements and extensions—are essential for practical stepwise development of complex software architectures.
Gonçalves RC, Sobral JL.  2012.  Modular and Non-Invasive Distributed Memory Parallelization. MISS '12: Proceedings of the 2012 workshop on Modularity in Systems Software. :33–38. Abstractgoncalves-2012.pdf

This paper presents an aspect-oriented library to support parallelization of Java applications for distributed memory environments, using a message-passing approach. The library was implemented using AspectJ language, and aims to provide a set of mechanisms to make easier to parallelize applications, as well as to solve well known problems of parallelization, such as lack of modularity and reusability. We compare the advantages of this method over the traditional approach, and we discuss differences to recent approaches that address the same problem. Results show benefits over other approaches, and, in most of cases, a competitive performance.
Masci P, Furniss D, Curzon P, Harrison M, Blandford A.  2012.  Supporting Field Investigators with PVS: A Case Study in the Healthcare Domain. Software Engineering for Resilient Systems. 7527:150-164. Abstractmascipvsdistributed.pdf

This paper reports the lessons learnt about the benefits of using a formal verification tool like PVS to support field studies. The presentation is based on a field study in the healthcare domain which was designed to investigate the resilience of human behaviour in an oncology ward of a hospital. The automated reasoning tool PVS was used systematically to compare actual practice observed during the field study with normative behaviour described for example by user manuals for the devices involved. The approach helped (i) identify latent situations that could lead to hazard, and (ii) suggest situations likely to warrant further investigation as part of the field study. The main contribution of this paper is a set of detailed examples that illustrate how we used PVS during the field study, and how the tool led to insights.

Masci P, Huang H, Curzon P, Harrison M.  2012.  Using PVS to Investigate Incidents through the Lens of Distributed Cognition. NASA Formal Methods. 7226:273-278. Abstractmascinasa.pdf

A systematic tool-based method is outlined that raises questions about the circumstances surrounding an incident: why it happened and what went wrong. The approach offers a practical and systematic way to apply a distributed cognition perspective to incident investigations, focusing on how available information resources (or the lack of them) may shape user action, rather than just on causal chains. This perspective supports a deeper understanding of the more systemic causes of incidents. The analysis is based on a higher order-logic model describing how information resources may have influenced the actions of those involved in the incident. The PVS theorem proving system is used to identify situations where available resources may afford unsafe user actions. The method is illustrated using a healthcare case study.
Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P.  2012.  Safer "5-key" number entry user interfaces using differential formal analysis. BCS HCI. :29-38. Abstract

Differential formal analysis is a new user interface analytic evaluation method based on stochastic user simulation. The method is particularly valuable for evaluating safety critical user interfaces, which often have subtle programming issues. The approach starts with the identification of operational design features that define the design space to be explored. Two or more analysts are required to analyse all combinations of design features by simulating keystroke sequences containing keying slip errors. Each simulation produces numerical values that rank the design combinations on the basis of their sensitivity to keying slip errors. A systematic discussion of the simulation results is performed for assessing the causes of any discrepancy, either in numerical values or rankings. The process is iterated until outcomes are agreed upon. In short, the approach combines rigorous simulation of user slip errors with diversity in modelling and analysis methods.

Although the method can be applied to other types of user interface, it is demonstrated through a case study of 5-key number entry systems, which are a common safety critical user interface style found in many medical infusion pumps and elsewhere. The results uncover critical design issues, and are an important contribution of this paper since the results provide device manufacturers guidelines to update their device firmware to make their devices safer.
Masci P, Ruksenas R, Huang H, Curzon P, Harrison M.  2012.  Formal verification and the prevention of systematic user error. FormalH, Workshop on Formal Methods in Human-Machine Interaction sponsored by the IFIP Working Group 13.5 on Human Error, Safety, and System Development.
Fernandes S, Cerone A, Barbosa LS, Papadopoulos PM.  2012.  FLOSS in Technology-Enhanced Learning. 1st International Symposium on Innovation and Sustainability in Education (InSuEDU 2012). Abstract

This paper presents a comparative analysis of Free/Libre Open Source Software (FLOSS) Learning Management System (LMS). Following a selection process we analyze the functionalities and characteristics of 8 tools commonly used in formal and informal education. More specifically we focus on the availability of different tools concerning communication and assistance, such as, forum, email, calendar, portfolios, etc. Our analysis showed that despite their similarities, the appropriateness of different FLOSS LMSs can be greatly affected by the specific needs of students, instructors and institutions.
Nassif L, Santiago JC, Nogueira JM.  2012.  Project Portfolio Selection in Public Administration using Fuzzy Logic. Selected papers from the 26th IPMA (International Project Management Association), World Congress.
Silva JMC, Lima SR.  2012.  Multiadaptive Sampling for Lightweight Network Measurements. 2012 21st International Conference on Computer Communications and Networks (ICCCN). :1-7. Abstract
n/a
Silva JMC, Lima SR.  2012.  Improving Network Measurement Efficiency through Multiadaptive Sampling. Traffic Monitoring and Analysis: 4th International Workshop, TMA 2012, Vienna, Austria, March 12, 2012. Proceedings. :171–174. Abstract

n/a
Silva JMC, Lima SR.  2012.  Optimizing Network Measurements through Self-adaptive Sampling. 2012 IEEE 14th International Conference on High Performance Computing and Communication 2012 IEEE 9th International Conference on Embedded Software and Systems. :794-801. Abstract
n/a
Cunha J, Visser J, Alves T, Saraiva JA.  2011.  Type-Safe Evolution of Spreadsheets. Fundamental Approaches to Software Engineering - FASE. 6603:186–201. Abstractfase11.pdf

Spreadsheets are notoriously error-prone. To help avoid the introduction of errors when changing spreadsheets, models that capture the structure and interdependencies of spreadsheets at a conceptual level have been proposed. Thus, spreadsheet evolution can be made safe within the confines of a model. As in any other model/instance setting, evolution may not only require changes at the instance level but also at the model level. When model changes are required, the safety of instance evolution can not be guarded by the model alone. We have designed an appropriate representation of spreadsheet models, including the fundamental notions of formulæand references. For these models and their instances, we have designed coupled transformation rules that cover specific spreadsheet evolution steps, such as the insertion of columns in all occurrences of a repeated block of cells. Each model-level transformation rule is coupled with instance level migration rules from the source to the target model and vice versa. These coupled rules can be composed to create compound transformations at the model level inducing compound transformations at the instance level. This approach guarantees safe evolution of spreadsheets even when models change.
Cunha J, Fernandes JP, Mendes J, Saraiva JA.  2011.  Embedding and Evolution of Spreadsheet Models in Spreadsheet Systems. Proceedings of the Symposium on Visual Languages and Human-Centric Computing - VL/HCC. :186–201. Abstractvl-hcc11.pdf

This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are wellknown and describe the business logic of spreadsheet data. We embed this domain specific model representation on the (general purpose) spreadsheet system it models. By defining such an embedding, we provide end users a model-driven engineering spreadsheet developing environment. End users can interact with both the model and the spreadsheet data in the same environment. Moreover, we use advanced techniques to evolve spreadsheets and models and to have them synchronized. In this paper we present our work on extending a widely used spreadsheet system with such a model-driven spreadsheet engineering environment.
Beckwith L, Cunha J, Fernandes JP, Saraiva JA.  2011.  End-users Productivity in Model-based Spreadsheets: An Empirical Study. Proceedings of the Third International Symposium on End-User Development - IS-EUD. :282–288. Abstractis-eud11.pdf

Spreadsheets are widely used and studies show that most of the existing ones contain non-trivial errors. To improve end-users productivity, recent research proposes the use of a model-driven engineering approach to spreadsheets. In this paper we conduct the first empirical study to assess the effectiveness and efficiency of this approach. A set of spreadsheet end users worked with two different model-based spreadsheets. We present and analyze here the results achieved.
Beckwith L, Cunha J, Fernandes JP, Saraiva JA.  2011.  An Empirical Study on End-users Productivity Using Model-based Spreadsheets. Proceedings of the European Spreadsheet Risks Interest Group. :87–100. Abstracteusprig11.pdf

Spreadsheets are widely used, and studies have shown that most end-user spreadsheets contain nontrivial errors. To improve end-users productivity, recent research proposes the use of a model-driven engineering approach to spreadsheets. In this paper we conduct the first systematic empirical study to assess the effectiveness and efficiency of this approach. A set of spreadsheet end users worked with two different model-based spreadsheets, and we present and analyze here the results achieved.