A Formal Approach to Specification, Analysis and Implementation of Policy-Based Systems

The design of modern computing systems largely exploits structured sets of declarative rules called policies. Their principled use permits controlling a wide variety of system aspects and achieving separation of concerns between the managing and functional parts of systems. These so-called policy-based systems are utilised within different application domains, from network management and autonomic computing to access control and emergency handling. The various policy-based proposals from the literature lack however a comprehensive methodology supporting the whole life-cycle of system development: specification, analysis and implementation. In this thesis we propose formally-defined tool-assisted methodologies for supporting the development of policy-based access control and autonomic computing systems. We first present FACPL, a formal language that defines a core, yet expressive syntax for the specification of attribute-based access control policies. On the base of its denotational semantics, we devise a constraint-based analysis approach that enables the automatic verification of different properties of interest on policies. We then present PSCEL, a FACPL-based formal language for the specification of autonomic computing systems. FACPL policies are employed to enforce authorisation controls and context-dependent adaptation strategies. To statically point out the effects of policies on system behaviours, we rely again on a constraint-based analysis approach and reason on progress properties of PSCEL systems. The implementation of the languages and their analyses provides us some practical software tools. The effectiveness of the proposed solutions is illustrated through real-world case studies from the e-Health and autonomic computing domains