Monitoring Interfaces for Faults

We consider the problem of a module interacting with an external interface (environment) where the interaction is expected to satisfy some system specification Φ. While we have the full implementation details of the module, we are only given a partial external specification for the interface. The interface specification being partial (incomplete) means that the interface displays only a strict subset of the behaviors allowed by the interface specification.Based on the assumption that interface specifications are typically incomplete, we address the question of whether we can tighten the interface specification into a strategy, consistent with the given partial specification, that will guarantee that all possible interactions resulting from possible behaviors of the module will satisfy the system specification Φ. We refer to such a tighter specification as Φ-guaranteeing specification. Rather than verifying whether the interface, which is often an off-the-shelf component, satisfies the tighter specification, the paper proposes a construction of a run-time monitor which continuously checks the existence of a Φ-guaranteeing interface.We view the module and the external interface as players in a 2-player game. The interface has a winning strategy if it can guarantee that no matter what the module does, the overall specification Φ is met. The problem of incomplete specifications is resolved by allowing the interface to follow any strategy consistent with the interface specification. Our approach essentially combines traditional run-time monitoring and static analysis. This allows going beyond the focus of traditional run-time monitoring tools – error detection in the execution trace, towards the focus of the static analysis – bug detection in the programs.     

Timers for Distributed Systems

We deal with temporal aspects of distributed systems, introducing and studying a new model called timed distributed π-calculus. This model extends distributed π-calculus with timers, transforming the communication channels into temporary resources. Distributed π-calculus describes located interactions between processes with restricted access to resources. We introduce time constraints by considering timeout timers for channels. Combining these timers with types and locations, we provide a formal framework able to describe complex systems with constraints on time and on resource access. Its typing system and operational semantics are presented. It is proved that the passage of time does not interfere with the typing system. The new model is proved to be sound by using a method based on subject reduction.     

UppDMC: A Distributed Model Checker for Fragments of the μ-Calculus

We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and μ-calculus specifications with at most one alternation of minimal and maximal fixed-point operators. This fragment is also known as . Recently, efficient game-based algorithms for this logic have been outlined.We describe the implementation of these algorithms within UppDMC and study their performance on practical examples. Running UppDMC on a simple workstation cluster, we were able to check liveness properties of the largest examples given in the VLTS Benchmark Suite, for which no answers were previously known.     

On the Jacopini Technique

The general concern of the Jacopini technique is the question: “Is it consistent to extend a given lambda calculus with certain equations?” The technique was introduced by Jacopini in 1975 in his proof that in the untyped lambda calculusΩis easy, i.e.,Ωcan be assumed equal to any other (closed) term without violating the consistency of the lambda calculus. The presentations of the Jacopini technique that are known from the literature are difficult to understand and hard to generalise. In this paper we generalise the Jacopini technique for arbitrary lambda calculi. We introduce the concept ofproof-replaceabilityby which the structure of the technique is simplified considerably. We illustrate the simplicity and generality of our formulation of the technique with some examples. We apply the Jacopini technique to theλμ-calculus, and we prove a general theorem concerning the consistency of extensions of theλμ-calculus of a certain form. Many well known examples (e.g., the easiness ofΩ) are immediate consequences of this general theorem.     

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic – and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model.     

Proving refinement using transduction

Summary. When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary. An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.     

An Algorithm for Finding the K-Best Allocations of a Tree Structured Program

We consider the problem of allocating n tasks of a distributed program to m processors of a distributed system in order to minimize total communication and processing costs. If the intertask communication can be represented by a tree and if the communication costs are uniform, it is known that an optimal allocation can be determined in O(nm) time. A K-optimal solution set Ω = { ₁,..., _K} of a given task allocation problem is a set of allocations such that no allocation which is not contained in Ω is better than any _i, i = 1,..., K. In this paper, an algorithm is presented which computes a K-optimal set for the considered task allocation problem in O(Knm).     

Merging Results for Distributed Content Based Image Retrieval

Searching information through the Internet often requires users to separately contact several digital libraries, use each library interface to author the query, analyze retrieval results and merge them with results returned by other libraries. Such a solution could be simplified by using a centralized server that acts as a gateway between the user and several distributed repositories: The centralized server receives the user query, forwards the user query to federated repositories—possibly translating the query in the specific format required by each repository—and fuses retrieved documents for presentation to the user. To accomplish these tasks efficiently, the centralized server should perform some major operations such as: resource selection, query transformation and data fusion. In this paper we report on some aspects of MIND, a system for managing distributed, heterogeneous multimedia libraries (MIND, 2001, http://www.mind-project.org). In particular, this paper focusses on the issue of fusing results returned by different image repositories. The proposed approach is based on normalization of matching scores assigned to retrieved images by individual libraries. Experimental results on a prototype system show the potential of the proposed approach with respect to traditional solutions.     

Concept-lexeme-syntax triangles: A gateway to interlingual translation

NABU is a large, multilingual Natural Language Processing (NLP) system being developed at MCC for Human Interface applications. Although the NABU project is not considering Machine Translation (MT) as an implementation domain, it is not unreasonable to suppose that, given our multilingual orientation, some MT problems could be ameliorated if not solved by our theoretical approach. This paper addresses the problem of MT via thecognitive interlingua method, focusing on the representation of the lexicon in such a system, and its accommodation of various sources of knowledge for use by both man and machine: notably, in the latter case, morphology, syntax, and semantics. We propose a new theoretical framework — the NABU Word Lattice — as a means of integrating multiple sources of knowledge in a parsimonious fashion conducive to formal interpretation within, and the construction of, an MT system.