Publications

Parisaca Vargas A, Garis A, Tarifa SLT, George C.  2009.  Model Checking LTL Formulae in RAISE with FDR. Integrated Formal Methods. 5423:231-245. Abstractifm09.pdf

The Raise Specification Language (RSL) is a modeling language which supports various specification styles. To apply model checking to RSL concurrent descriptions, we translate RSL specifications into the input language CSPM of FDR. FDR is the model checker for the process algebra CSP. First, we define a syntactic and semantic translation from the concurrent applicative subset of RSL to CSPM, and show that this translation is a strong bisimulation which preserves properties such as traces and deadlock. Consequently, results obtained by refinement checks in FDR are sound for the original RSL descriptions. Second, RSL uses Linear Temporal Logic (LTL) to specify desired properties, but FDR does not support LTL. LTL formulas may be translated to CSP test processes in order to check them with FDR. We build a tool which automates the translation of RSL specifications into CSPM and translates LTL formulas to CSP processes, enabling the model checking of LTL formulas over RSL descriptions with FDR.
Harrison M, Campos JC, Loer K.  2008.  Formal analysis of interactive systems: opportunities and weaknesses. Research Methods in Human Computer Interaction. :88-111. Abstract

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.
Harrison M, Campos JC, Doherty G, Loer K.  2008.  Connecting rigorous system analysis to experience centred design. Maturing Usability: Quality in Software, Interaction and Value. :56-74. Abstract

The chapter explores the role that formal modelling may play in aiding the visualisation and implementation of usability with a particular emphasis on experience requirements in an ambient and mobile system. Mechanisms for requirements elicitation and evaluation are discussed, as well as the role of scenarios and their limitations in capturing experience requirements. The chapter then discusses the role of formal modelling by revisiting an analysis based on an exploration of traditional usability requirements before moving on to consider requirements more appropriate to a built environment. The role of modelling within the development process is re-examined by looking at how models may incorporate knowledge relating to user experience and how the results of the analysis of such models may be exploited by human factors and domain experts in their consideration Ambient and mobile systems are often used to bring information and services.
Oliveira JN.  2008.  Transforming Data by Calculation. Generative and Transformational Techniques in Software Engineering 2007. 5235:134-195. Abstract

This paper addresses the foundations of data-model transformation. A catalog of data mappings is presented which includes abstraction and representation relations and associated constraints. These are justified in an algebraic style via the pointfree-transform, a technique whereby predicates are lifted to binary relation terms (of the algebra of programming) in a two-level style encompassing both data and operations. This approach to data calculation, which also includes transformation of recursive data models into “flat” database schemes, is offered as alternative to standard database design from abstract models. The calculus is also used to establish a link between the proposed transformational style and bidirectional lenses developed in the context of the classical view-update problem.
Jorge AM, Poças J, Azevedo PJ.  2008.  A Methodology for Visual Exploration of Association Models. Visual Data Mining: Theory, Techniques and Tools for Visual Analytics. Abstract

Visualization in data mining is typically related to data exploration. In this chapter we present a methodology for the post processing and visualization of association rule models. One aim is to provide the user with a tool that enables the exploration of a large set of association rules. The method is inspired by the hypertext metaphor. The initial set of rules is dynamically divided into small comprehensible sets or pages, according to the interest of the user. From each set, the user can move to other sets by choosing one appropriate operator. The set of available operators transform sets of rules into sets of rules, allowing focusing on interesting regions of the rule space. Each set of rules can also be then seen with different graphical representations. The tool is web-based and dynamically generates SVG pages to represent graphics. Association rules are given in PMML format.
Backhouse R, Ferreira JF.  2008.  Recounting the Rationals: Twice!. Mathematics of Program Construction (LNCS 5133). Abstract

We derive an algorithm that enables the rationals to be efficiently enumerated in two different ways. One way is known and is credited to Moshe Newman; it corresponds to a deforestation of the so-called Calkin-Wilf tree of rationals. The second is new and corresponds to a deforestation of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Newman’s algorithm.
Almeida PS, Moreno CB, Fonte V.  2007.  Improving on version stamps. On the Move to Meaningful Internet Systems 2007: OTM 2007 Workshops. 4806:1025–1031. Abstract

Optimistic distributed systems often rely on version vectors or their variants in order to track updates on replicated objects. Some of these mechanisms rely on some form of global configuration or distributed naming protocol in order to assign unique identifiers to each replica. These approaches are incompatible with replica creation under arbitrary partitions, a typical operation mode in mobile or poorly connected environments. Other mechanisms assign unique identifiers relying on statistical correctness. In previous work we have introduced an update tracking mechanism that overcomes these limitations. This paper presents results from recent experimentation, that brought to surface a particular pattern of operation that results in an unforeseen, unlimited growth in space consumption. We also describe informally a new update tracking mechanism that does not exhibit this pathological growth while providing guaranteed unique identifiers for a dynamic number of replicas under arbitrary partitions and the same functionality of version vectors.
Barbosa LS, Martinho M.  2007.  Modelling is for reasoning. Mathematical Modelling (ICTMA 12): Education, Engineering and Economics. :480-490. Abstract

In a broad sense, computing is an area of knowledge from which a popular and effective technology emerged long before a solid, specific, scientific methodology, let alone formal foundations, had been put forward. This might explain some of the weaknesses in the software industry, on the one hand, as well as an excessively technology-oriented view which dominates computer science training at pre-university and even undergraduate teaching, on the other. Modelling, understood as the ability to choose the right abstractions for a problem domain, is consensually recognised as essential for the development of true engineering skills in this area, as it is in all other engineering disciplines. But, how can the basic problem-solving strategy, one gets used to from school physics: understand the problem, build a mathematical model, reason within the model, calculate a solution, be taken (and taught) as the standard way of dealing with software design problems? This paper addresses this question, illustrating and discussing the interplay between modelling and reasoning.
Ferreira P, Azevedo PJ.  2007.  Deterministic Motif Mining in Protein Databases. Successes and New Directions in Data Mining. Abstract

Protein sequence motifs describe, through means of enhanced regular expression syntax, regions of amino acids that have been conserved across several functionally related proteins. These regions may have an implication at the structural and functional level of the proteins. Sequence motif analysis can bring significant improvements towards a better understanding of the protein sequence-structure-function relation. In this chapter, we review the subject of mining deterministic motifs from protein sequence databases. We start by giving a formal definition of the different types of motifs and the respective specificities. Then, we explore the methods available to evaluate the quality and interest of such patterns. Examples of applications and motif repositories are described. We discuss the algorithmic aspects and different methodologies for motif extraction. A brief description on how sequence motifs can be used to extract structural level information patterns is also provided.
Campos JC, Harrison M.  2006.  Automated deduction and usability reasoning. Encyclopedia of Human-Computer Interaction. :45-54. Abstract

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.
Fernandes A, Pereira JR, Campos JC.  2006.  Accessibility and Visually Impaired Users. Enterprise Information Systems VI. Abstract

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.
Oliveira JN, Rodrigues C.  2006.  Pointfree Factorization of Operation Refinement. FM - Formal Methods 2006 . 4085:236–251. Abstract

The standard operation refinement ordering is a kind of “meet of op- posites”: non-determinism reduction suggests “smaller” behaviour while increase of definition suggests “larger” behaviour. Groves’ factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathe- matically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and ex- ploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed.
Cunha A, Oliveira JN, Visser J.  2006.  Type-safe two-level data transformation . FM 2006: Formal Methods. 4085:284-299. Abstract

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution coupled with document migration, and data mappings used for interoperability and persistence.
We provide a formal treatment of two-level data transformations that is type-safe in the sense that the well-formedness of the value-level transformations with respect to the type-level transformation is guarded by a strong type system. We rely on various techniques for generic functional programming to implement the formalization in Haskell.
The formalization addresses various two-level transformation scenarios, covering fully automated as well as user-driven transformations, and allowing transformations that are information-preserving or not. In each case, two-level transformations are disciplined by one-step transformation rules and type-level transformations induce value-level transformations. We demonstrate an example hierarchical-relational mapping and subsequent migration of relational data induced by hierarchical format evolution.
Cortes B, Oliveira JN.  2006.  Relational Sampling for Data Quality Auditing and Decision Support. Enterprise Information Systems V. :82–88. Abstract

This paper presents a strategy for applying sampling techniques to relational databases, in the context of data quality auditing or decision support processes. Fuzzy cluster sampling is used to survey sets of records for correctness of business rules. Relational algebra estimators are presented as a data quality-auditing tool.
Barbosa LS, Sun M, Aichernig B, Rodrigues N.  2006.  On the Semantics of Componentware: a Coalgebraic Perspective. Mathematical Frameworks for Component Software: Models for Analysis and Synthesis. :69–117. Abstract

In this chapter we present a coalgebraic semantics for components. Our semantics forms the basis for a family of operators for combining components. These operators together with their algebraic laws establish a calculus for software components. We present two applications of our semantics: a coalgebraic interpretation of UML diagrams and the design of a component repository.