A FACPL-based Language for Self-Adaptive Policy-based Autonomic Computing Systems
PSCEL is a formal language that takes a holistic approach to programming and regulating autonomic computing systems. PSCEL is a full-fledged instantiation of SCEL and advocates a design of self-adaptive, autonomic systems based on dynamically generated ensembles of basic components.
The PSCEL components are the building blocks of the systems and represent the computational units whose dynamical organisation forms the ensembles. Each component includes an interface, a knowledge repository, a process and a policy.
- Processes define the computational behaviour of components.
- Policies aim at regulating the actions performed by the processes and possibly adapt component behaviours.
- Interfaces expose different component features and contextual values that can be used to dynamically establish the partners of an interaction, thus providing flexible and expressive communication mechanisms.
- Knowledge repositories store the data known to the system components, including, e.g., information about their state and working environment.
The policy language FACPL is used as the specification formalism for the component policies. Indeed, it is possible to define policies implementing adaptation strategies by exploiting specific actions that are produced at runtime as an effect of policy evaluation. These actions are executed as part of component behaviours to enforce system adaptation.
- A Formal Approach to Specification, Analysis and Implementation of Policy-based Systems (PhD Thesis) A. Margheri. 2016
- Design, Analysis and Implementation Policy-Based Self-Adaptive Computing Systems (Technical Report) A. Margheri, H. Riis Nielson, F. Nielson, R. Pugliese. Technical Report, 2016
- Towards Static Analysis of Policy-Based Self-Adaptive Computing Systems A. Margheri, H. Riis Nielson, F. Nielson, R. Pugliese. In Proc. of the 7th International Symposium Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (ISoLA 2016), 2016. Springer.
- On Programming and Policing Autonomic Computing Systems M. Loreti, A. Margheri, R. Pugliese, F. Tiezzi. In Proc. of the 6th International Symposium Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (ISoLA 2014), 2014. Springer.
- Linguistic Abstractions for Programming and Policing Autonomic Computing Systems A. Margheri, R. Pugliese, F. Tiezzi. In Proc. of the 10th International Conference on Autonomic and Trusted Computing (ATC 2013), 2013. IEEE.
3. Supporting Tools: jRESP and Flow Analysis
jRESP: A Java Runtime Environment
(Main developer Michele Loreti)
The jRESP Java runtime environment offers a set of APIs for the development of self-adaptive, autonomic systems based on PSCEL.
The PSCEL IDE is an Eclipse plug-in offering a tailored development environment for PSCEL. It supports with graphical features the coding of PSCEL code and permits automated generation of runnable jRESP and SMT-LIB code. The SMT-LIB code is used, together with the Z3 SMT solver, to define the Policy-Flow graph. See this paper for further details.
- Eclipse Update Site http://facpl.sourceforge.net/pscel/release/0.9/ (to be used from the Eclipse Command: "Install New Software...")
- Xtext Code on Sourceforge
An Essential User's Guide for the IDE
- Install the PSCEL Eclipse Plugin by using the update site http://facpl.sourceforge.net/pscel/release/0.9/
- Create a new Plug-in Project
- Open the MANIFEST.MF
- Add the following two plug-ins to the 'Required Plug-ins' part of the 'Dependencies' tab
- Create a new text file with extension .pscel
- When requested, convert the project to the 'Xtext' nature
- Code in PSCEL and save
- Add the generated src-gen folder to the Build Path (Use as a Source Folder)
PSCEL Analysis: Policy-Flow graph
- To create the Policy-Flow graph: run the java classes in the package *.flowgraphs
- To visualise the graph use the dot tool provided by the graphviz tool
Samples of visualised Policy-Flow graphs are as follows
4. Security Analysis of PSCEL Policies
PSCEL policies are used to enforce both adaptation and authorisation strategies. To analyse the effects on PSCEL systems of adaptation strategies, we have defined the Policy-Flow graph and its exploitation. Instead, to analyse the effects of the authorisation strategies, thus carrying out a security analysis, we can leverage on the FACPL analysis tools. The tools permits verifying properties on the authorisation granted by the considered policies to PSCEL actions.
To this aim, it is possible to use the FACPL Eclipse IDE, but some minor modifications have to be applied to PSCEL policies for enabling their analysis. Further details follow.
Indeed, as PSCEL policies are written according to a dialect of FACPL, some rearranging of PSCEL-oriented constructs have to be done. We report in the following list the needed rearrangements.
- Adhere to FACPL keywords, i.e. "policy" -> "PolicySet", "rules:"-> "policies:" (by using the Eclipse auto-completion commands, you can simply achieve the task).
- Remove policy parameters (by possibly replacing them with attribute names).
- Put PSCEL distinguished values (e.g, put and this) as string values.
- Using a customised target function for pattern_match comparison (see example below for definition).
- Align obligation definitions introducing an effect
At the following links, an example of a PSCEL policy and its FACPL translation are available.
5. Main Contributors
Associate Professor at University of Firenze, Dipartimento di Statistica, Informatica e Applicazioni
Associate Professor at University of Camerino, School of Science and Technology
Associate Researcher at University of Firenze, Dipartimento di Statistica, Informatica e Applicazioni