Abstract

Abstract
In the domain of machines' design, one of the most important issues to solve is related with the controller's design, mainly, guaranteeing that the machine will behave as expected. In order to achieve a dependable controller, some steps can be considered, such as the formalization of its specification-before being translated to the program that will be inserted in the controller device-and the respective analysis and verification. Nowadays, some formal analysis techniques, such as formal verification, are used to achieve this purpose. The dependability of a controller, however, is impacted by its execution context. This paper proposes an approach for the formal verification of the specification of mechatronic system's controllers, which considers, on the formal verification tasks, the behavior of the plant and the behavior of the Human Machine Interface of the Mechatronic system. Some conclusions are extrapolated for other systems of the same kind.

Abstract

Abstract
.Abstract algebra has the power to unify seemingly disparate theories once they are encoded into the same abstract formalism. This paper shows how a relation-algebraic rendering of both database dependency theory and Hoare programming logic purports one such unification, in spite of the latter being an algorithmic theory and the former a data theory. The approach equips relational data with functional types and an associated type system which is useful for database operation type checking and optimization. The prospect of a generic, unified approach to both programming and data theories on top of libraries already available in automated deduction systems is envisaged.

Abstract
Device miniaturization is pointing towards tolerating imperfect hardware provided it is "good enough". Software design theories will have to face the impact of such a trend sooner or later. A school of thought in software design is relational: it expresses specifications as relations and derives programs from specifications using relational algebra. This paper proposes that linear algebra be adopted as an evolution of relational algebra able to cope with the quantification of the impact of imperfect hardware on (otherwise) reliable software. The approach is illustrated by developing a monadic calculus for component oriented software construction with a probabilistic dimension quantifying (by linear algebra) the propagation of imperfect behaviour from lower to upper layers of software systems. © 2014 Springer International Publishing.

Abstract
Deduplication of primary storage volumes in a cloud computing environment is increasingly desirable, as the resulting space savings contribute to the cost effectiveness of a large scale multi-tenant infrastructure. However, traditional archival and backup deduplication systems impose prohibitive overhead for latency-sensitive applications deployed at these infrastructures while, current primary deduplication systems rely on special cluster filesystems, centralized components, or restrictive workload assumptions. We present DEDIS, a fully-distributed and dependable system that performs exact and cluster-wide background deduplication of primary storage. DEDIS does not depend on data locality and works on top of any unsophisticated storage backend, centralized or distributed, that exports a basic shared block device interface. The evaluation of an open-source prototype shows that DEDIS scales out and adds negligible overhead