Redundancy is a system property that generally refers to duplication of state information or system function. While redundancy is usually investigated in the context of fault tolerance, one can argue that it is in fact an intrinsic feature of a system that can be analyzed on its own without reference to fault tolerance. Redundancy may arise by design, generally to support fault tolerance, or as a natural byproduct of design, and is usually unexploited. In this paper, we tentatively explore observable forms of redundancy, as well as mathematical models that capture them.

We propose Kleene algebra with domain (KAD), an extension of Kleene algebra by simple equational axioms for a domain and a codomain operation. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of programs and state transition systems. We develop the basic calculus, present the most interesting models and discuss some related theories. We demonstrate applicability by two examples: algebraic reconstructions of Noethericity and propositional Hoare logic based on equational reasoning.

Echoing Louis Pasteur's quote, we submit the premise that it is advantageous to define measures of distance between requirements specifications because such measures open up a wide range of possibilities both in theory and in practice. The authors present a mathematical basis for measuring distances between specifications and show how their measures of distance can be used to address concrete problems that arise in the practice of software engineering.

We give a formal relation-based definition of scenarios and we show how different scenarios can be integrated to obtain a more global view of user-system interactions. We restrict ourselves to the sequential case, meaning that we suppose that there is only one user (thus, the scenarios we wish to integrate cannot occur concurrently). Our view of scenarios is state-based, rather than event-based, like most of the other approaches, and can be grafted to the well-established specification language Z. Also, the end product of scenario integration, the specification of the functional aspects of the system, is given as a relation; this specification can be refined using independently developed methods. Our formal description is coupled with a diagram-based, transition-system like, presentation of scenarios, which is better suited to communication between clients and specifiers.

Given a software library whose entries are represented by formal specifications, we distinguish between two retrieval procedures: exact retrieval, whereby, given a query K, we identify all the library components that are correct with respect to K; approximate retrieval, which is invoked when exact retrieval fails, and identifies the library components that minimize adaptation effort. To this effect, we define four measures of functional distance between specifications, and discuss algorithms that minimize these measures over a set of components; then we discuss whether these measures can be used to predict adaptation effort.