RADAR: Ring-based adaptive discovery of active neighbour routers

in Lecture Notes in Computer Science (2002, December), 2546

The RADAR protocol and its underlying neighbourhood discovery framework extend the ANTS toolkit by giving active nodes the ability to discover dynamically other active nodes close to them without relying ... [more ▼]

The RADAR protocol and its underlying neighbourhood discovery framework extend the ANTS toolkit by giving active nodes the ability to discover dynamically other active nodes close to them without relying on any configuration file. Such an automatic discovery is the key to administration of large or sparse active networks and the first step towards an efficient active routing. Active nodes will use their local IP routing table to run an extended ring search in their domain. An Additive Increase Multiplicative Decrease control allows RADAR to discover several neighbours per physical interface without searching too far away or fixing a maximum distance a priori. The protocol is complemented by a traffic-driven discovery that can grab capsules coming from unknown nodes (mainly outside the local domain) and trigger targetted probing of those addresses. [less ▲]

Characterizing simpler recognizable sets of integers

in Lecture Notes in Computer Science (2002), 2420

For the k-ary numeration system, we characterize the sets of integers such that the corresponding representations make up a star-free regular language. This result can be transposed to some linear ... [more ▼]

For the k-ary numeration system, we characterize the sets of integers such that the corresponding representations make up a star-free regular language. This result can be transposed to some linear numeration systems built upon a Pisot number like the Fibonacci system and also to k-adic numeration systems. Moreover we study the problem of the base dependence of this property and obtain results which are related to Cobham's Theorem. [less ▲]

Counting the Solutions of Presburger Equations without Enumerating Them

in Lecture Notes in Computer Science (2001), 2494

The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of ... [more ▼]

The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of arbitrary Presburger formulas, or the set of reachable states of some systems using unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of vectors represented as an NDD. We give an algorithm that is able to perform an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, we also develop an efficient projection method that allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. Our algorithms have been implemented in the verification tool LASH, and applied successfully to various counting problems. [less ▲]

Constitutive equations and numerical modelling of time effects in soft porous rocks

in Lecture Notes in Computer Science (2001), 1988

A constitutive model is developed within the framework of Perzyna's viscoplasticity for predicting the stress-strain-time behaviour of soft porous rocks. The model is based on the hyperelasticity and ... [more ▼]

A constitutive model is developed within the framework of Perzyna's viscoplasticity for predicting the stress-strain-time behaviour of soft porous rocks. The model is based on the hyperelasticity and multisurface viscoplasticity with hardening. A time-stepping algorithm is presented for integrating the creep sensitive law. An example of application to one-dimensional consolidation is presented. The objectives are to: 1. present a soft rock model which is capable of taking into account the rate sensitivity, time effects and creep rupture; 2. to discuss the use of an incremental procedure for time stepping using large time increments and 3. to extend the finite element code Lagamine (MSM-ULg) for viscoplastic problems in geomechanics. [less ▲]

An Active Layered Multicast Adaptation Protocol

in Lecture Notes in Computer Science (2000, October 16), 1942

We describe an active application in the field of multicast congestion control for real-time traffic. Our Active Layered Multicast Adaptation Protocol is a layered multicast congestion control scheme ... [more ▼]

We describe an active application in the field of multicast congestion control for real-time traffic. Our Active Layered Multicast Adaptation Protocol is a layered multicast congestion control scheme built on top of an Active Network infrastructure. It benefits from router support in order to obtain information about resources available and to perform the adaptation tasks at the places where shortage of resources occur. It supports heterogeneous receivers through the combination of layered multicast transmission with selective filtering and pruning of layers within the active nodes. Market-based resource management ideas are applied to achieve a resource utilisation level that represents an equilibrium between the user goals and the node operator goals. Our simulation results show that the protocol is feasible and provides adequate reactions to short term and persistent congestion, while keeping the amount of state and processing in the active nodes limited. [less ▲]

On the construction of automata from linear arithmetic constraints

in Lecture Notes in Computer Science (2000, March), 1785

This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed ... [more ▼]

This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed allows a linear-time determinization procedure to be used. Furthermore, it shows through theoretical analysis and experiments that the special structure of the constructed automata does, in quite a general way, render the usual upper bounds on automata operations vastly overpessimistic. [less ▲]

Verifying Systems with Infinite but Regular State Spaces

in Lecture Notes in Computer Science (1998), 1427

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems ... [more ▼]

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems. This has prompted efforts to apply a similar approach to systems with infinite state spaces. Doing so amounts to developing algorithms for computing a symbolic representation of the infinite state space, as opposed to requiring the user to characterize the state space by assertions. Of course, in most cases, this can only be done at the cost of forgoing any general guarantee of success. The goal of this paper is to survey a number of results in this area and to show that a surprisingly common characteristic of the systems that can be analyzed with this approach is that their state space can be represented as a regular language. [less ▲]

Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs

in Lecture Notes in Computer Science (1997), 1217

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination ... [more ▼]

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination problems between the concurrent processes of a system. In this paper, we present a method to synthesize a finite-state machine that simulates all the sequences of visible operations of a given process that were observed during a state-space exploration performed by VeriSoft. The examination of this machine makes it possible to discover the dynamic behavior of the process in its environment and to understand how it contributes to the global behavior of the system. [less ▲]

The Power of QDDs

in Lecture Notes in Computer Science (1997), 1302

Queue-content Decision Diagrams (QDDs) are finite-automaton based data structures for representing (possibly infinite) sets of contents of a finite collection of unbounded FIFO queues. Their intended use ... [more ▼]

Queue-content Decision Diagrams (QDDs) are finite-automaton based data structures for representing (possibly infinite) sets of contents of a finite collection of unbounded FIFO queues. Their intended use is to serve as a symbolic representation of the possible queue contents that can occur in the state space of a protocol modeled by finite-state machines communicating through unbounded queues. This is done with the help of a loop-first search, a state-space exploration technique that attempts whenever possible to compute symbolically the effect of repeatedly executing a loop any number of times, making it possible to analyze protocols with infinite state spaces though without the guarantee of termination. This paper first solves a key problem concerning the use of QDDs in this context: it precisely characterizes when, and shows how, the operations required by a loop-first search can be applied to QDDs. Then, it addresses the problem of exploiting QDDs and loop-first searches to broaden the range of properties that can be checked from simple state reachability to temporal logic. Finally, a sufficient criterion for the termination of a loop-first search using QDDs is given. [less ▲]

Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs

in Lecture Notes in Computer Science (1996), 1102

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that ... [more ▼]

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most "real" protocols. Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented. A loop-first search using QDDs has been implemented, and experiments on several existing communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state spaces. [less ▲]