A Maude Formalization of Object Nets.

Self-adaptive systems gain growing attention by raising service quality and reducing development costs. But on the other hand, self-adaptation is a source of complexity that needs suitable methodologies/models/tools supporting the entire life cycle. A particularly challenging point is the dynamic reconfiguration of a system. This feature, typical of modern distributed systems, has led to the definition of specialized formalisms, e.g. the pi-calculus or Nets-within-Nets, which essentially build on top of the concept of a changing system structure. But even with syntactic sugar, these formalisms differ enough from the ‘daily’ programming languages. This work aims to bridge the gap between theory and practice by introducing an abstract machine for the base type of Nets-within-Nets. Our encoding is in the well-known Maude language, whose rewriting logic semantics ensures the mathematical soundness needed for analysis and an intuitive operational perspective.