Thesis Abstract
Typically, policy-based management systems formulate policies as sets of Event-Condition-Action (ECA) rules. ECA rules specify the action to be executed when a certain event-condition combination is observed by a system. The problem with ECA rules is that they do not contain any explicit specifications of actions and therefore very little reasoning can be done with them.
ECA rules are used to specify database triggers, access-control policies and management policies. Advanced reasoning and guarantees are provided by systems using the first two kinds of rules while very weak guarantees are provided by systems enforcing management policies. The reason is that the set of actions used in triggers and access-control policies are well-defined and therefore implicitly their specifications are known. Since actions in management policies are not well-defined and can be simple atomic operations to complex scripts, explicitly specifying the action behavior enables similar reasoning to be performed with management policies.
Therefore, I am proposing a specification-enhanced ECA model called Event-Condition-Precondition-Action-Postcondition (ECPAP) for formulating management policies. Rules in this framework contain axiomatic specifications of actions in First-Order Temporal Logic. This enables conflict analysis due to side-effects of actions, termination analysis, confluence analysis, guaranteeing enforcement semantics, enforcement verification, policy refinement and policy exception handling. In addition, the ECPAP framework can be extended to have behavioral specifications of actions, which enables providing guarantees for policies with persistent actions such as QoS, heartbeats and so on. The presence of specifications also allows development of policy debugging and profiling tools.
Existing policy-based management systems exhibit non-deterministic behavior. My thesis argues that deterministic behavior is essential for effective policy-based management and I demonstrate in my dissertation that ECPAP model enables determinism for policy-based systems.