Specification and Analysis of the AERNCA Active Network Protocol Suite in RealTime Maude This paper describes the application of the RealTime Maude tool and the Maude formal methodology to the specification and analysis of the AERNCA suite of active network multicast protocol components. Because of the timesensitive and resourcesensitive behavior and the composability of its components, AERNCA poses challenging new problems for its formal specification and analysis. RealTime Maude is a natural extension of the Maude rewriting logic language and tool for the specification and analysis of realtime objectbased distributed systems. It supports a wide spectrum of formal methods, including: executable specification; symbolic simulation; and infinitestate model checking of temporal logic formulas. These methods complement those offered by finitestate model checkers and generalpurpose theorem provers. RealTime Maude has proved to be wellsuited to meet the AERNCA modeling challenges, and its methods have been effective in uncovering subtle and important errors in the informal use case specification.

Reactive Actors: Isolation for Efficient Analysis of Distributed Systems In this paper we explain how the isolation or decoupling of actors can help in developing efficient analysis techniques. The Reactive Object Language, Rebeca, and its timed extension are introduced as actorbased languages for modeling and analyzing distributed systems. We show how floatingtime transition system can be used for model checking of timed actor models when we are interested in eventbased properties, and how it helps in state space reduction. We explain how the model of computation of actors helps in devising an efficient state distribution policy in distributed model checking. We show how we use Rebeca to verify the routing algorithms of mobile adhoc networks. The paper is written in a way to make the ideas behind each technique clear such that it can be reused in similar domains.