Abstraction reduces the problem of whether an infinite state system satisfies a temporal logic property to model checking that property on a finite state abstract version. The most common abstractions are quotients of the original system. We present a simple method of defining quotient abstractions by means of equations collapsing the set of states. Our method yields the minimal quotient system together with a set of proof obligations that guarantee ...
At present, designers of real-time systems face a dilemma between expressiveness and automatic verification: if they can specify some aspects of their system in some automaton-based formalism, then automatic verification is possible; but more complex system components may be hard or impossible to express in such decidable formalisms. These more complex components may still be simulated; but there is then little support for their formal analysis. The main goal of ...
This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analysis of the AER/NCA suite of active network multicast protocol components. Because of the time-sensitive and resource-sensitive behavior, the presence of probabilistic algorithms, and the composability of its components, AER/NCA poses challenging new problems for its formal specification and analysis. Real-Time Maude is a natural extension of the Maude rewriting logic ...
The increasing importance, criticality, and complexity of communications software makes very desirable the application of formal methods to gain high assurance about its correctness. These needs are even greater in the context of active networks, because the difficulties involved in ensuring critical properties such as security and safety for dynamically adaptive software are substantially higher than for more static software approaches. There are in fact many obstacles to the insertion ...
The main goal was to learn through simulation about the functionality and performance on realistic applications of an RRM system consisting of a collection of RRM ensemble chips (each such chip being a SIMD processor) connected on a network, and to design mechanisms to support the simultaneous parallel computation of applications across many such ensemble chips. To achieve these goals we first built a high-level interensemble simulator and ran a ...
Reports by Author
