Recent Publications

Avvenuti M, Corsini P, Masci P, Vecchio A.  2007.  Energy-efficient reception of large preambles in MAC protocols for wireless sensor networks. Electronics Letters. 43:300–301. Abstract

A technique able to significantly reduce the energy consumption of contention-based MAC protocols for wireless sensor networks is presented. Address and timing information is embedded into the packet preamble, allowing receivers to power off their radio during part of the transmission. Analytical and experimental evaluations show a significant extension of the network lifetime.

Mano A, Campos JC.  2006.  Usabilidade em interfaces para crianças. Jornal de Circunstâncias Cognitivas. Abstractjcc_v2.pdf

O estudo da interacção entre crianças e computadores tem recebido atenção crescente nos últimos anos (ver, por exemplo, a série de conferências em Interaction Design and Children). A utilização de meios informáticos, quer para actividades educativas, quer para actividades de lazer (bem como a sua integração), tem um potencial genericamente reconhecido. No entanto, é necessário estudar de que forma as crianças interpretam e interagem com as interfaces se pretendemos desenvolver sistemas bem sucedidos.
O objectivo do estudo apresentado nesta comunicação consistiu exactamente em estudar o modo como crianças entre os 5 e os 7 anos de idade interagem com computadores. Tal como mencionado, existe já investigação nesta área, e alguns conjuntos de guidelines de desenho estão já publicados (por exemplo, Gilutz e Nielsen, 2002). A diferença entre o presente estudo e outras publicações reside na forma como os dados serão obtidos e nos próprios objectivos do estudo. A principal meta do método utilizado não é descobrir o que as crianças podem ou não fazer numa interface, mas sim os motivos pelos quais elas conseguem ou não utilizá-la.

Barbosa LS, Oliveira JN.  2006.  Transposing Partial Components: an Exercise on Coalgebraic Refinement. Theoretical Computer Science. 365:2-22. Abstractbo06_lsb.pdf

A partial component is a process which fails or dies at some stage, thus exhibiting a finite, more ephemeral behaviour than expected (eg, operating system crash). Partiality --- which is the rule rather than exception in formal modelling --- can be treated mathematically via totalization techniques. In the case of partial functions, totalization involves error values and exceptions. In the context of a coalgebraic approach to component semantics, this paper argues that the behavioural counterpart to such functional techniques should extend behaviour with try-again cycles preventing from component collapse, thus extending totalization or transposition from the algebraic to the coalgebraic context. We show that a refinement relationship holds between original and totalized components which is reasoned about in a coalgebraic approach to component refinement expressed in the pointfree binary relation calculus. As part of the pragmatic aims of this research, we also address the factorization of every such totalized coalgebra into two coalgebraic components --- the original one and an added front-end --- which cooperate in a client-serverstyle.

Rodrigues N, Barbosa LS.  2006.  Component Identification Through Program Slicing. Electronic Notes in Theoretical Computer Science. 160:291-304. Abstractcips_nfr.pdf

This paper reports on the development of specific slicing techniques for functional programs and their use for the identification of possible coherent components from monolithic code. An associated tool is also introduced. This piece of research is part of a broader project on program understanding and re-engineering of legacy code supported by formal methods.

Ribeiro P, Barbosa LS.  2006.  Generic process algebra: A programming challenge. Journal of Universal Computer Science. 12:922–937. Abstractrbb06_lsb.pdf

Emerging interaction paradigms, such as service-oriented computing, and new technological challenges, such as exogenous component coordination, suggest new roles and application areas for process algebras. This, however, entails the need for more generic and adaptable approaches to their design. For example, some applications may require similar programming constructs coexisting with different interaction disciplines. In such a context, this paper pursues a research programme on a coinductive rephrasal of classic process algebra, proposing a clear separation between structural aspects and interaction disciplines. A particular emphasis is put on the study of interruption combinators defined by natural co-recursion. The paper also illustrates the verification of their properties in an equational and pointfree reasoning style as well as their direct encoding in Haskell.

Rodrigues N, Barbosa LS.  2006.  Program Slicing by Calculation. Journal of Universal Computer Science. 12:828–848. Abstractrb06_lsb.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 oriented towards the imperatice or object 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.

Bernardeschi C, Lettieri G, Martini L, Masci P.  2006.  Using postdomination to reduce space requirements of data flow analysis. Information Processing Letters. 98:11–18.
Bernardeschi C, Lettieri G, Martini L, Masci P.  2006.  Using Control Dependencies for Space-Aware Bytecode Verification. Computer Journal. 49:234–248. Abstract

Java applets run on a Virtual Machine that checks code integrity and correctness before execution using a module called the Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. The large memory requirements of the verification process do not allow the implementation of an embedded Bytecode Verifier in the Java Card Virtual Machine. To address this problem, we propose a verification algorithm that optimizes the use of system memory by imposing an ordering on the verification of the instructions. This algorithm is based on control flow dependencies and immediate postdominators in control flow graphs.

Barbosa MB, Cunha A, Pinto JS.  2005.  Recursion Patterns and Time-analysis. SIGPLAN Notices. 40(5):45–54. Abstractrecpta.pdf

This paper explores some ideas concerning the time-analysis of functional programs defined by instantiating typical recursion patterns such as folds, unfolds, and hylomorphisms. The concepts in this paper are illustrated through a rich set of examples in the Haskell programming language. We concentrate on unfolds and folds (also known as anamorphisms and catamorphisms respectively) of recursively defined types, as well as the more general hylomorphism pattern. For the latter, we use as case-studies two famous sorting algorithms, mergesort and quicksort. Even though time analysis is not compositional, we argue that splitting functions to expose the explicit construction of the recursion tree and its later consumption helps with this analysis.

Cunha A, Pinto JS.  2005.  Point-free Program Transformation. Fundamenta Informaticae. 66(4):315–352. Abstractpfpt.pdf

The subject of this paper is functional program transformation in the so-called point-free style. By this we mean first translating programs to a form consisting only of categorically-inspired combinators, algebraic data types defined as fixed points of functors, and implicit recursion through the use of type-parameterized recursion patterns. This form is appropriate for reasoning about programs equationally, but difficult to actually use in practice for programming. In this paper we present a collection of libraries and tools developed at Minho with the aim of supporting the automatic conversion of programs to point-free (embedded in Haskell), their manipulation and rule-driven simplification, and the (limited) automatic application of fusion for program transformation.

Cruz A, Barbosa LS, Oliveira JN.  2005.  From Algebras to Objects: Generation and Composition. Journal of Universal Computer Science. 11:1580–1612. Abstractjucs_11_10_1580_1612_cruz_lsb.pdf

This paper addresses objectification, a formal specification technique which inspects the potential for object-orientation of a declarative model and brings the 'implicit objects' explicit. Criteria for such objectification are formalized and implemented in a runnable prototype tool which embeds Vdm-sl into Vdm++. The paper also includes a quick presentation of a (coinductive) calculus of such generated objects, framed as generalised Moore machines.

Sun M, Aichernig B, Barbosa LS, Naixião Z.  2005.  A Coalgebraic Semantic Framework for Component Based Development in UML. Electronic Notes in Theoretical Computer Science. 122:229-245. Abstract1-s2.0-s1571066105000411-main.pdf

This paper introduces a generic semantic framework for component-based development, expressed in the unified modelling language UML. The principles of a coalgebraic semantics for class, object and statechart diagrams as well as for use cases, are developed. It is also discussed how to formalize the refinement steps in the development process based upon a suitable notion of behavior refinement. In this way, a formal basis for component-based development in UML is studied, which allows the construction of more complex and specific systems from independent components.

Meng S, Barbosa LS.  2005.  Components as coalgebras: The refinement dimension. Theoretical Computer Science. 351:276-294. Abstractmb05_1.pdf

This paper characterizes refinement of state-based software components modeled as pointed coalgebras for some Set endofunctors. The proposed characterization is parametric on a specification of the underlying behaviour model introduced as astrong monad. This provides a basis to reason about (and transform) state-based software designs. In particular it is shown how refinement can be applied to the development of the inequational subset of a calculus of generic software components.

Rodrigues N, Barbosa LS.  2005.  Architectural Prototyping: From CCS to Net. Electronic Notes in Theoretical Computer Science. 130:151–167. Abstractrb05final_lsb.pdf

Over the last decade, software architecture emerged as a critical issue in Software Engineering. This encompassed a shift from traditional programming towards software development based on the deployment and assembly of independent components. The specification of both the overall systems structure and the interaction patterns between their components became a major concern for the working developer. Although a number of formalisms to express behaviour and to 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 CCS behavioural specifications the corresponding architectural skeletons in the Microsoft .Net framework, in the form of executable C and C# code. The prototyping process is fully supported by a specific tool developed in Haskell. Keywords: Software architecture; prototyping; CCS; Net framework, in the form of executable C# and Cω code. The prototyping process is fully supported by a specific tool developed in Haskell.

Garis A, Albornoz C, Riesco D, Montejano G, Debnath N.  2005.  Development of a Tool for Code Automatic Generation of Persistent Objects. Journal Computing Methods in Science and Engineering. 5(1472-7978):85–92. Abstract

The presented CASE tool makes persistent classes generation easy. The tool is a bridge between object oriented languages and relational databases. Generated persistent classes contain database access code. The programmer use this classes to instantiate objects with persistence facilities. In this way the tool allows to automate and improve part of the process of software development.