We propose a model for specifying, ana\-lysing and enforcing safe usage of resources. Our usage policies allow for parametricity over resources, and they can be enforced through finite state automata. The patterns of resource access and creation are described through a basic calculus of usages. In spite of the augmented flexibility given by resource creation and by policy parametrization, we devise an efficient (polynomial-time) model-checking technique for deciding when a usage is resource-safe, i.e.\ when it complies with all the relevant usage policies.
Model checking usage policies
BARTOLETTI, MASSIMO;
2009-01-01
Abstract
We propose a model for specifying, ana\-lysing and enforcing safe usage of resources. Our usage policies allow for parametricity over resources, and they can be enforced through finite state automata. The patterns of resource access and creation are described through a basic calculus of usages. In spite of the augmented flexibility given by resource creation and by policy parametrization, we devise an efficient (polynomial-time) model-checking technique for deciding when a usage is resource-safe, i.e.\ when it complies with all the relevant usage policies.
I metadati presenti in IRIS UNICA sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono protetti da diritto d'autore, salvo diversa indicazione.
