Specification of a partial replication protocol with TLA+

Nowadays, data available and used by companies is growing very fast creating the need to use and manage this data in the most efficient way. To this end, data is replicated overmultiple datacenters and use different replication protocols, according to their needs, like more availability or stronger consistency level. The costs associated with full data replication can be very high, and most of the times, full replication is not needed since information can be logically partitioned. Another problem, is that by using datacenters to store and process information clients become heavily dependent on them. We propose a partial replication protocol called ParTree, which replicates data to clients, and organizes clients in a hierarchy, using communication between them to propagate information. This solution addresses some of these problems, namely by supporting partial data replication and offline execution mode. Given the complexity of the protocol, the use of formal verification is crucial to ensure the protocol two correctness properties: causal consistency and preservation of data. The use of TLA+ language and tools to formally specificity and verify the proposed protocol are also described.

Introducing mapping standards in the quality assessment of buildings extracted from very high resolution satellite imagery

Many municipal activities require updated large-scale maps that include both topographic and thematic information. For this purpose, the efficient use of very high spatial resolution (VHR) satellite imagery suggests the development of approaches that enable a timely discrimination, counting and delineation of urban elements according to legal technical specifications and quality standards. Therefore, the nature of this data source and expanding range of applications calls for objective methods and quantitative metrics to assess the quality of the extracted information which go beyond traditional thematic accuracy alone. The present work concerns the development and testing of a new approach for using technical mapping standards in the quality assessment of buildings automatically extracted from VHR satellite imagery. Feature extraction software was employed to map buildings present in a pansharpened QuickBird image of Lisbon. Quality assessment was exhaustive and involved comparisons of extracted features against a reference data set, introducing cartographic constraints from scales 1:1000, 1:5000, and 1:10,000. The spatial data quality elements subject to evaluation were: thematic (attribute) accuracy, completeness, and geometric quality assessed based on planimetric deviation from the reference map. Tests were developed and metrics analyzed considering thresholds and standards for the large mapping scales most frequently used by municipalities. Results show that values for completeness varied with mapping scales and were only slightly superior for scale 1:10,000. Concerning the geometric quality, a large percentage of extracted features met the strict topographic standards of planimetric deviation for scale 1:10,000, while no buildings were compliant with the specification for scale 1:1000.

Proposta de um modelo de medição e análise da satisfação de clientes em empresas de software : caso prático do ambiente business-to-business

Os estudos da satisfação e lealdade do cliente em ambiente Business-to-Business têm emergido devido ao interesse práctico e académico. Recorreu-se a um caso práctico de uma empresa de software internacional, ESRI, a operar em Portugal com modelo de negócio B2B e comportamento de compra extensivo. Desenvolveu-se um modelo estrutural com 11 variáveis latentes: lealdade; satisfação; imagem; atmosfera; cooperação; adaptação; processos; tecnologia; orientação ao cliente; competências; colaboradores e comunicação. Foram analisadas 304 respostas ao questionário de satisfação e de seguida aplicou-se o modelo a seis grupos de clientes segmentados de acordo com a contribuição do cliente para as receitas e o comportamento no processo de decisão de compra. Recorreu-se a modelos SEM (Structural Equation Modelling) com estimação dos parâmetros através da metodologia PLS (partial Least Squares). Os resultados mostram nos seis segmentos, que os valores da empresa, a cooperação através da competência dos colaboradores e da orientação ao cliente e a tecnologia são factores mais importantes para a satisfação e lealdade dos clientes.

HEP-Frame: A software engineered framework to aid the development and efficient multicore execution of scientific code

This work was supported by FCT (Fundação para a Ciência e Tecnologia) within Project Scope (UID/CEC/00319/2013), by LIP (Laboratório de Instrumentação e Física Experimental de Partículas) and by Project Search-ON2 (NORTE-07-0162- FEDER-000086), co-funded by the North Portugal Regional Operational Programme (ON.2 - O Novo Norte), under the National Strategic Reference Framework, through the European Regional Development Fund.

A domain-specific language for ETL patterns specification in Data Warehousing Systems

During the last few years many research efforts have been done to improve the design of ETL (Extract-Transform-Load) systems. ETL systems are considered very time-consuming, error-prone and complex involving several participants from different knowledge domains. ETL processes are one of the most important components of a data warehousing system that are strongly influenced by the complexity of business requirements, their changing and evolution. These aspects influence not only the structure of a data warehouse but also the structures of the data sources involved with. To minimize the negative impact of such variables, we propose the use of ETL patterns to build specific ETL packages. In this paper, we formalize this approach using BPMN (Business Process Modelling Language) for modelling more conceptual ETL workflows, mapping them to real execution primitives through the use of a domain-specific language that allows for the generation of specific instances that can be executed in an ETL commercial tool.

Using relational algebra on the specification of real world ETL processes

Modeling Extract-Transform-Load (ETL) processes of a Data Warehousing System has always been a challenge. The heterogeneity of the sources, the quality of the data obtained and the conciliation process are some of the issues that must be addressed in the design phase of this critical component. Commercial ETL tools often provide proprietary diagrammatic components and modeling languages that are not standard, thus not providing the ideal separation between a modeling platform and an execution platform. This separation in conjunction with the use of standard notations and languages is critical in a system that tends to evolve through time and which cannot be undermined by a normally expensive tool that becomes an unsatisfactory component. In this paper we demonstrate the application of Relational Algebra as a modeling language of an ETL system as an effort to standardize operations and provide a basis for uncommon ETL execution platforms.

Improving quality of medical service with mobile health software

An increasing number of m-Health applications are being developed benefiting health service delivery. In this paper, a new methodology based on the principle of calm computing applied to diagnostic and therapeutic procedure reporting is proposed. A mobile application was designed for the physicians of one of the Portuguese major hospitals, which takes advantage of a multi-agent interoperability platform, the Agency for the Integration, Diffusion and Archive (AIDA). This application allows the visualization of inpatients and outpatients medical reports in a quicker and safer manner, in addition to offer a remote access to information. This project shows the advantages in the use of mobile software in a medical environment but the first step is always to build or use an interoperability platform, flexible, adaptable and pervasive. The platform offers a comprehensive set of services that restricts the development of mobile software almost exclusively to the mobile user interface design. The technology was tested and assessed in a real context by intensivists.

Refinement and variability techniques in model transformation of software requirements

Tese de Doutoramento em Tecnologias e Sistemas de Informação

Specification and testing of multiplicative time-varying GARCH models with applications

In this article, we develop a specification technique for building multiplicative time-varying GARCH models of Amado and Teräsvirta (2008, 2013). The variance is decomposed into an unconditional and a conditional component such that the unconditional variance component is allowed to evolve smoothly over time. This nonstationary component is defined as a linear combination of logistic transition functions with time as the transition variable. The appropriate number of transition functions is determined by a sequence of specification tests. For that purpose, a coherent modelling strategy based on statistical inference is presented. It is heavily dependent on Lagrange multiplier type misspecification tests. The tests are easily implemented as they are entirely based on auxiliary regressions. Finite-sample properties of the strategy and tests are examined by simulation. The modelling strategy is illustrated in practice with two real examples: an empirical application to daily exchange rate returns and another one to daily coffee futures returns.

Estudo e implementação de testes de software em desenvolvimento ágil

Dissertação de mestrado em Engenharia de Sistemas

Conversão sistemática do comportamento definido nos blocos funcionais da norma IEC 61 131-3 para autómatos finitos temporizados

Dissertação de mestrado integrado em Engenharia Mecânica

Frameworks no desenvolvimento de software: o caso da Elevation da PRIMAVERA BSS

Dissertação de mestrado integrado em Engenharia e Gestão de Sistemas de Informação

Feature Nets: behavioural modelling of software product lines

Software product lines (SPL) are diverse systems that are developed using a dual engineering process: (a)family engineering defines the commonality and variability among all members of the SPL, and (b) application engineering derives specific products based on the common foundation combined with a variable selection of features. The number of derivable products in an SPL can thus be exponential in the number of features. This inherent complexity poses two main challenges when it comes to modelling: Firstly, the formalism used for modelling SPLs needs to be modular and scalable. Secondly, it should ensure that all products behave correctly by providing the ability to analyse and verify complex models efficiently. In this paper we propose to integrate an established modelling formalism (Petri nets) with the domain of software product line engineering. To this end we extend Petri nets to Feature Nets. While Petri nets provide a framework for formally modelling and verifying single software systems, Feature Nets offer the same sort of benefits for software product lines. We show how SPLs can be modelled in an incremental, modular fashion using Feature Nets, provide a Feature Nets variant that supports modelling dynamic SPLs, and propose an analysis method for SPL modelled as Feature Nets. By facilitating the construction of a single model that includes the various behaviours exhibited by the products in an SPL, we make a significant step towards efficient and practical quality assurance methods for software product lines.