Books

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.