Model Checking Starvation for Resource-aware Active Objects with Coloured Petri Nets

Abstract

Dynamic resource provisioning is an important driver for pay-on-demand cloud computing. Virtualized resources open for resource awareness, such that applications may use resource management strategies to modify their deployment resource consumption at run-time. The ABS language supports the modeling of deployment decisions and resource management for active objects. An important property in this context is to ensure that the resource management does not lead to starvation of the executing objects. In previous work, we have formally translated the semantics of the ABS language into a parameterized Coloured Petri Net (CPN) model, such that any ABS program can be represented by setting the initial marking accordingly. In this paper, we characterize starvation using Computation Tree Logic (CTL), and demonstrate how CTL model checking of the CPN encoding of the ABS model, in combination with path finding, can be used to detect starvation and synthesize load balancers that guarantee starvation freedom