Specification and Prototyping of Reactive Distributed Systems with Algebraic Term Nets

The specification of the dynamic behaviour of reactive distributed systems must exhibit the structures of control andhas to imply explicitly the relevant aspects of the distribution, such as the concurrency, the reactivity and the interactionbetween the entities. Among the most common reactive distributed systems we can cite industrial ones; distributednetworks 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 fortrustworthy systems has received tremendous researchers’ attention. The usage of formal tools for simulation andprototyping designed to facilitate the modelling of such systems is of great interest. Improved methods are needed to insurereliability, security and robustness of industrial distributed systems. This paper proposes the fundamentals of a formalapproach for the specification of reactive distributed systems based on object-oriented paradigm. Object’s behaviour ismodelled as REACTNets. The REACTNets enhance the ECATNets that are a kind of high level algebraic Petri nets withexplicit distribution and reactivity. We associate to the classic ECATNets MAUDE rules to handle interactions betweenobjects. The two formalisms have a common semantics in term of rewriting logic so that interesting prospects are opened fortheir integration