Recent Publications

Alves T, Silva P, Visser J, Oliveira JN.  2005.  Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion. FM - Proceedings of International Symposium of Formal Methods Europe. 3582:399-414. Abstractfm05.pdf

We constructed a tool, called VooDooM, which converts datatypes in VDM-SL into SQL relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction.
The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward.

Pereira JO, Oliveira R.  2005.  Rewriting 'The Hare and the Turtle': Sleeping to Get There Faster. Proceedings of the 35th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) (Supplemental Volume). Abstracthareturtle_jop.pdf

When developing algorithms for dependable distributed systems one often makes several simplifying assumptions that are essential to reason about the problem in hand. It is usual to assume an asynchronous system model, unconstrained system resources and the absence of easily maskable faults such as message loss. While most of the simplifications strengthen the model and are particularly useful when proving theoretical edge results, asynchrony, on the contrary, is a "non-assumption" and it is specially appealing in practice as it yields robust solutions that are correct regardless of the actual timing behavior of the target systems.

Sousa AL, Pereira JO, Soares L, Correia A, Rocha L, Oliveira R, Moura F.  2005.  Testing the dependability and performance of group communication based database replication protocols. Proceedings of 35th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). Abstractdbsim-dsn-pds05.pdf

Database replication based on group communication systems has recently been proposed as an efficient and resilient solution for large-scale data management. However, its evaluation has been conducted either on simplistic simulation models, which fail to assess concrete implementations, or on complete system implementations which are costly to test with realistic large-scale scenarios. This paper presents a tool that combines implementations of replication and communication protocols under study with simulated network, database engine, and traffic generator models. Replication components can therefore be subjected to realistic large scale loads in a variety of scenarios, including fault-injection, while at the same time providing global observation and control. The paper shows first how the model is configured and validated to closely reproduce the behavior of a real system, and then how it is applied, allowing us to derive interesting conclusions both on replication and communication protocols and on their implementations.

Correia A, Sousa AL, Soares L, Pereira JO, Moura F, Oliveira R.  2005.  Group-based replication of on-line transaction processing servers. Proceedings of 2nd Latin-American Symposium on Dependable Computing (LADC). 3747 Abstractladc05.pdf

Several techniques for database replication using group communication have recently been proposed, namely, the Database State Machine, Postgres- R, and the NODO protocol. Although all rely on a totally ordered multicast for consistency, they differ substantially on how multicast is used. This re- sults in different performance trade-offs which are hard to compare as each protocol is presented using a different load scenario and evaluation method. In this paper we evaluate the suitability of such protocols for replication of On-Line Transaction Processing (OLTP) applications in clusters of servers and over wide area networks. This is achieved by implementing them using a common infra-structure and by using a standard workload. The results allows us to select the best protocol regarding performance and scalability in a demanding but realistic usage scenario.

Visser J, Oliveira JN, Barbosa LS, Ferreira JF, Mendes A.  2005.  Camila Revival: VDM meets Haskell. Proceedings of Overture Workshop . Abstract2005-camilarevival.pdf

We have experimented with modeling some of the key concepts of the VDM specification language inside the functional programming language Haskell. For instance, VDM’s sets and maps are directly available as data types defined in standard libraries; we merely needed to define some additional functions to make the match complete. A bigger challenge is posed by VDM’s data type invariants, and pre- and post- conditions. For these we resorted to Haskell’s constructor class mechanism, and its support for monads. This allows us to switch between different modes of evaluation (e.g. with or without property checking) by simply coercing user defined functions and operations to different specific types.

Sun M, Barbosa LS, Naixião Z.  2005.  On Refinement of Software Architectures. Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings. 3722:469–484. Abstractmbz05.pdf

Although increasingly popular, software component techniques still lack suitable formal foundations on top of which rigorous methodologies for the description and analysis of software architectures could be built. This paper aims to contribute in this direction: building on previous work by the authors on coalgebraic semantics, it discusses component refinement at three different but interrelated levels: behavioural, syntactic, i.e., relative to component interfaces, and architectural. Software architectures are defined through component aggregation. On the other hand, such aggregations, no matter how large and complex they are, can also be dealt with as components themselves, which paves the way to a discipline of hierarchical design. In this context, a major contribution of this paper is the introduction of a set of rules for architectural refinement.

Rodrigues N, Barbosa LS.  2005.  Slicing Functional Programs by Calculation. Beyond Program Slicing. 05451 Abstractoriginalprogramslicingcalc16443.pdf

Program slicing is a well known family of techniques used to identify code fragments which depend on or are depended upon specific program entities. They are particularly useful in the areas of reverse engineering, program understanding, testing and software maintenance. Most slicing methods, usually targeting either the imperative or the object oriented paradigms, are based on some sort of graph structure representing program dependencies. Slicing techniques amount, therefore, to (sophisticated) graph transversal algorithms. This paper proposes a completely different approach to the slicing problem for functional programs. Instead of extracting program information to build an underlying dependencies’ structure, we resort to standard program calculation strategies, based on the so-called Bird-Meertens formalism. The slicing criterion is specified either as a projection or a hiding function which, once composed with the original program, leads to the identification of the intended slice. Going through a number of examples, the paper suggests this approach may be an interesting, even if not completely general alternative to slicing functional programs.

Barbosa LS, Rodrigues N.  2005.  Prototyping Concurrent Systems in C Omega. IVNET - First International Conference of Innovative Views of NET Technologies. Abstractrb05-pcscw_p.pdf

Software architecture is currently recognized as one of the most critical design steps in Software Engineering. The specification of the overall system structure, on the one hand, and of the interactions patterns between its components, on the other, became a major concern for the working developer. Although a number of formalisms to express behaviour and supply the indispensable calculational power to reason about designs, are available, the task of deriving architectural designs on top of popular component platforms has remained largely informal. This paper introduces a systematic approach to derive, from behavioural specifications written in Cw, the corresponding architectural skeletons in the Microsoft .NET framework in the form of executable code.

Campos JC.  2004.  The modelling gap between software engineering and human-computer interaction. ICSE Workshop: Bridging the Gaps II. :54-61. Abstracticse04.pdf

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.

Campos JC.  2004.  Análise de usabilidade baseada em modelos. Interação 2004 - 1a. Conferência Nacional em Interação Pessoa-Máquina. :171-176. Abstractint04.pdf

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.

Fernandes A, Pereira JO, Campos JC.  2004.  Accessibility and Visually Impaired Users. ICEIS - Proceedings of the 6th International Conference on Enterprise Information Systems. 5:75-80. Abstracticeis04.pdf

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.

Mano A, Campos JC.  2004.  A study about usability criteria on computer interfaces for children. 1st Portuguese Forum of Experimental Psychology. Abstracthandout.pdf

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.

Mano A, Campos JC.  2004.  Aplicação de um Cognitive Walkthrough - estudo de caso. Interação 2004 - 1a. Conferência Nacional em Interação Pessoa-Máquina. :256-258. Abstractint04-mano.pdf

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.

Campos JC, Harrison M, Loer K.  2004.  Verifying user interface behaviour with model checking. Verification and Validation of Enterprise Information Systems (VVEIS 2004). :87-96. Abstract10.1.1.131.5872.pdf

A large proportion of problems found in deployed systems relate to the user interface. This paper presents an approach to the verification of user interface models based on model checking. The approach is intended to be used early in design. The verification is concerned with behavioural aspects of the user interface and requires models that represent both the interactive aspects and also capture important features of the context to allow restrictions of behaviour to those that conform to appropriate human and environmental constraints. A tool suite to support the approach is under development and is described. Future work directions are put forward.

Rodrigues L, Pereira JO.  2004.  Self-Adapting Epidemic Broadcast Algorithms (extended abstract). FuDiCo II: S.O.S. Survivability: Obstacles and Solutions - 2nd Bertinoro Workshop on Future Directions in Distributed Computing. Abstract10.1.1.190.491.pdf

Epidemic broadcast algorithms have a number of characteristics, such as strong resilience to node failures, that make them an appealing technology to build survivable systems. However, the performance of existing protocols is highly dependent of runtime parameters, such as the network load or network topology. In the current extended abstract we advocate, using concrete illustrations, the use of self-adapting epidemic broadcast algorithms.