Computing Publications

Publications Home » Verification of Policy-based Self...

Verification of Policy-based Self-Managed Cell Interactions Using Alloy

Alberto Schaeffer Filho, Emil Lupu, Morris Sloman, Susan Eisenbach

Technical Report
April, 2009

Self-Managed Cells (SMCs) define an infrastructure for building ubiquitous computing applications. An SMC consists of an autonomous administrative domain based on a policy-driven feedback control-loop. SMCs are able to interact with each other and compose with other SMCs to form larger autonomous components. In this paper we present a formal specification of an SMC's behaviour for the analysis and verification of its operation in collaborations of SMCs. These collaborations typically involve SMCs originated from different administrative authorities, and the definition of a formal model has helped us to verify the correctness of their operation when SMCs are composed or federated. The formal specification also enables a better characterisation of the integrity constraints that must be preserved during SMC operation.

PDF of full publication (949 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.