Specification and Prototyping of Reactive Distributed Systems with Algebraic Term Nets

Abstract: The specification of the dynamic behaviour of reactive distributed systems must exhibit the structures of control and has to imply explicitly the relevant aspects of the distribution, such as the concurrency, the reactivity and the interaction between the entities. Among the most common reactive distributed systems we can cite industrial ones; distributed networks occur for example in telecommunications, Internet, power and energy, transportation and manufacturing. Distributed computing will play an increasingly critical role in the global industrial-infrastructure. The need for trustworthy systems has received tremendous researchers’ attention. The usage of formal tools for simulation and rototyping designed to facilitate the modelling of such systems is of great interest. Improved methods are needed to insure reliability, security and robustness of industrial distributed systems. This paper proposes the fundamentals of a formal approach for the specification of reactive distributed systems based on object-oriented paradigm. Object’s behaviour is modelled as REACTNets. The REACTNets enhance the ECATNets that are a kind of high level algebraic Petri nets with explicit distribution and reactivity. We associate to the classic ECATNets MAUDE rules to handle interactions between objects. The two formalisms have a common semantics in term of rewriting logic so that interesting prospects are opened for their integration.

Keywords: Reactive distributed systems, object oriented paradigm, rewriting logic, ECATNets, Maude, rapid prototyping.

 Received February 5, 2008; accepted September 1, 2008