FORMALIZING DISTRIBUTED SELF-ADAPTIVE SYSTEMS USING HIGH-LEVEL PETRI NETS

Formal models must be adequately supported by software tools in order to aid both the design and development of modern distributed systems. Such systems have a growing complexity due to advanced features, such as adaptive mechanisms, they are equipped with to deal with the dynamical environments in which they operate. In this paper, we introduce a two-layer formal model for self-adaptive distributed discrete-event systems, based on standard (Low- and High-level) Petri nets. This formal framework, supported by a modular software library called PNEMU, can be thought of as a baseline to formalize self-adaptation having a decentralized control. This paper focuses on the description of the model's operational semantics. Moreover, it outlines the structure and basic usage of PNEMU.