ETD system

Electronic theses and dissertations repository


Tesi etd-09162016-152055

Thesis type
Tesi di dottorato di ricerca
email address
A Formal Approach to Specification, Analysis and Implementation of Policy-Based Systems
Settore scientifico disciplinare
Corso di studi
tutor Prof. Pugliese, Rosario
Parole chiave
  • Formal Methods
  • SMT
  • Autonomic Computing
  • Policy Languages
  • Access Control
Data inizio appello
Riassunto analitico
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. <br><br>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. <br><br>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. <br><br>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. <br><br>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.<br>