A high-level petri net-based formal model of distributed self-adaptive systems

Engineering complex distributed self-adaptive systems is a challenging task due to multiple interacting distributed components that monitor and adapt the managed parts operating in a dynamic environment. Therefore, formal methods able to specify and analyze the behavior of decentralized adaptation control by multiple interacting MAPE-K (Monitor, Analyze, Plan, and Execute over a shared Knowledge) components are highly demanded. In this paper we introduce a formal framework for modeling and analyzing self-adaptive systems with decentralized adaptation control. The framework makes use of High-Level Petri nets which represents a sound and expressive formal model for distributed discrete-event systems. We show how to specify in a natural way structural changes that are likely to occur in adaptable and evolvable distributed applications. Our approach supports validation and verification activities to check correctness of the MAPE components. As a proof-of-concepts, we show how to use our framework to model and analyze a self-optimizing cluster management system.