Logic-based detection of conflicts in APPEL policies

Abstract

APPEL is a general language for expressing policies in a variety of application domains with a clear separation between the core language and its specialisation for concrete domains. Policies can conflict, thus leading to undesired behaviour. We present a novel formal semantics for the APPEL language based on ΔDSTL(×) (so far APPEL only had an informal semantics). ΔDSTL(×) is an extension of temporal logic to deal with global applications: it includes modalities to localize properties to system components, an operator to deal with events, and temporal modalities àla Unity. A further contribution of the paper is the development of techniques based on the semantics to reason about conflicts. © Springer-Verlag Berlin Heidelberg 2007.