Publications

Jesus P.  2016.  Robust Distributed Data Aggregation. AbstractBook Link

Distributed aggregation algorithms are an important building block of modern large scale systems, as it allows the determination of meaningful system-wide properties which are required to direct the execution of distributed applications. In the last decade, several algorithms have been proposed to address the distributed computation of aggregation functions, exhibiting different properties in terms of accuracy, speed and communication tradeoffs. However, existing approaches exhibit many issues when challenged in faulty and dynamic environments, lacking in terms of fault-tolerance and support to churn. This book studies the robust distributed aggregation problem. In particular, a definition of the aggregation problem is proposed, existing distributed aggregation algorithm are surveyed and classified into a comprehensive taxonomy, and a novel approach named Flow Updating which is fault-tolerant and able to operate on dynamics networks is detailed. This work is expected to constitute a relevant contribution to the area of distributed computing, in particular for the robust distributed computation of aggregation functions in dynamic networks.
Cerone A, Persico D, Papers R, Nikolova N, Stefanova E, Fernandes S.  2014.  Information Technology and Open Source: Applications for Education, Innovation, and Sustainability. :305p.70illus. AbstractWebsite

This book constitutes revised selected papers from the following SEFM 2012 satellite events: InSuEdu, the First International Symposium on Innovation and Sustainability in Education; MokMaSD, the First International Symposium on Modelling and Knowledge Management for Sustainable Development and Open Cert, the 6th International Workshop on Foundations and Techniques for Open Source Software Certification, held in Thessaloniki, Greece, in October 2012. The total of 14 regular papers and 7 short papers included in this volume were carefully reviewed and selected from 35 submissions. The papers cover the topics related to the use of Information and Communication Technology (ICT) and Open Source Software (OSS) as tools to foster and support Education, Innovation and Sustainability.
Cunha J.  2012.  Model-based Spreadsheet Engineering: Using Relational Models to Improve Spreadsheets. AbstractWebsite

Spreadsheets can be viewed as programming languages for non-professional programmers. These so-called "end-user'' programmers vastly outnumber professional programmers creating millions of new spreadsheets every year. As a programming language, spreadsheets lack support for abstraction, testing, encapsulation, or structured programming. As a result, and as numerous studies have shown, the high rate of production is accompanied by an alarming high rate of errors. Some studies report that up to 90% of real-world spreadsheets contain errors. After their initial creation, many spreadsheets turn out to be used for storing and processing increasing amounts of data and supporting increasing numbers of users over long periods of time, making them complicated systems.
An emerging solution to handle the complex and evolving software systems is Model-driven Engineering (MDE). To consider models as first class entities and any software artifact as a model or a model element is one of the basic principles of MDE.
We adopted some techniques from MDE to solve spreadsheet problems. Most spreadsheets (if not all) lack a proper specification or a model. Using reverse engineering techniques we are able to derive various models from legacy spreadsheets. We use functional dependencies (a formalism that allow us to define how some column values depend on other column values) as building blocks for these models. Models can be used for several spreadsheet improvements, namely refactoring, safe evolution, migration or even generation of edit assistance. The techniques presented in this work are available under the framework HAEXCEL that we developed. It is composed of online and batch tools, reusable HASKELL libraries and OpenOffice.org extensions.
A study with several end-users was organized to survey the impact of the techniques we designed. The results of this study indicate that the models can bring great benefits to spreadsheet engineering helping users to commit fewer errors and to work faster.
Bonchi F, Bonsangue M, Rutten J, Silva A.  2012.  Brzozowski's Algorithm (Co)Algebraically. Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday. 7230:12–23. AbstractWebsite

We give a new presentation of Brzozowski’s algorithm to minimize finite automata, using elementary facts from universal algebra and coalgebra, and building on earlier work by Arbib and Manes on the duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations.
Almeida JB, Frade MJ, Pinto JS, Sousa SM.  2011.  Rigorous Software Development: an introduction to program verification. AbstractWebsite

The use of mathematical methods in the development of software is essential when reliable systems are sought; in particular they are now strongly recommended by the official norms adopted in the production of critical software. Program Verification is the area of computer science that studies mathematical methods for checking that a program conforms to its specification. This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. The idea of specifying the behaviour of individual software components by attaching contracts to them is now a widely followed approach in program development, which has given rise notably to the development of a number of behavioural interface specification languages and program verification tools. A foundation for the static verification of programs based on contract-annotated routines is laid out in the book. These can be independently verified, which provides a modular approach to the verification of software. The text assumes only basic knowledge of standard mathematical concepts that should be familiar to any computer science student. It includes a self-contained introduction to propositional logic and first-order reasoning with theories, followed by a study of program verification that combines theoretical and practical aspects -- from a program logic (a variant of Hoare logic for programs containing user-provided annotations) to the use of a realistic tool for the verification of C programs (annotated using the ACSL specification language), through the generation of verification conditions and the static verification of runtime errors.
Farsi M, Barbosa MB.  2000.  CANopen Implementation: Application to Industrial Networks. Computers and Communications Series. AbstractWebsite

Fieldbus technology has long been recognised as the future in industrial control applications. This book is intended for those wishing to embark on implementing CANopen protocols in their products, system integrators and for those planning to do pre-conformance testing of their products before pursuing a certification authority.This book describes the application of CAN, the CANopen protocol and communication technology at the shop floor level.
Harrison M, Masci P, Campos JC, Curzon P.  2017.  The Specification and Analysis of Use Properties of a Nuclear Control System. The Handbook of Formal Methods in Human-Computer Interaction. Abstractp-00m-t6a.pdf

The chapter explores a layered approach to the analysis of the Nuclear Power Plant Control System described in Chapter 4. A model is specified to allow the analysis of use-centred properties based on generic templates. User interface properties include: the visibility of state attributes, the clarity of the mode structure and the ease with which an action can be recovered from. Property templates are used as heuristics to ease the construction of requirements for the control system interface.
da Silva CP, Lima SR, Silva JM.  2017.  Exploring SDN to Deploy Flexible Sampling-Based Network Monitoring. Internet of Things, Smart Spaces, and Next Generation Networks and Systems: 17th International Conference, NEW2AN 2017, 10th Conference, ruSMART 2017, Third Workshop NsCC 2017, St. Petersburg, Russia, August 28–30, 2017, Proceedings. :109–120. Abstract

In recent years we witnessed the arrival of new trends, such as server virtualization and cloud services, an increasing number of mobile devices and online contents, leading the networking industry to deliberate about how traditional network architectures can be adapted or even deciding if a new perspective for them should be taken. SDN (Software-Defined Networking) emerged under this framing, opening a road for new developments due to the centralized logic control and view of the network, the decoupling of data and control planes, and the abstraction of the underlying network infrastructure from the applications. Although firstly oriented to packet switching, network measurements have also emerged as one promising field for SDN, as its flexibility enables programmable measurements, allowing a SDN controller to manage measurement tasks concurrently at multiple spatial and temporal scales.
Ruksenas R, Masci P, Curzon P.  2016.  Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. From Action Systems to Distributed Systems: The Refinement Approach. wp325.pdf
Barbosa LS, Martins MA, Madeira A, Neves R.  2016.  Reuse and Integration of Specification Logics: The Hybridisation Perspective. Theoretical Information Reuse and Integration. 446:1–30. Abstractbmmn16.pdf

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.
Sanchez A, Barbosa LS, Madeira A.  2015.  Modelling and Verifying Smell-Free Architectures with the Archery Language. Software Engineering and Formal Methods. :147-163. Abstractsmellfreearch2014.pdf

Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smell-free using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.
Teixeira J, Couto M.  2015.  Automatic Distinction of Fernando Pessoas' Heteronyms. Progress in Artificial Intelligence: 17th Portuguese Conference on Artificial Intelligence, EPIA 2015, Coimbra, Portugal, September 8-11, 2015. Proceedings. :783–788. Abstractautomatic-distinction-fernando.pdf

n/a
Barbosa MB, Castro D, Silva P.  2014.  Compiling CAO: From Cryptographic Specifications to C Implementations. Principles of Security and Trust. 8414:240-244. Abstractpost14.pdf

We present a compiler for CAO, an imperative DSL for the cryptographic domain. The tool takes high-level cryptographic algorithm specifications and translates them into C implementations through a series of security-aware transformations and optimizations.
The compiler back-end is highly configurable, allowing the targeting of very disparate platforms in terms of memory requirements and computing power.