Formal verification in autonomic-component ensembles

摘要

Autonomic computing systems (or hosting datacenters) have attracted a lot of attention in recent years. Large data centers provide services to many customers by sharing available IT resources. Each customer typically has a service level agreement (SLA), which specifies constraints on performance and/or quality of service that it receives from the system. The quality of the autonomic computing policies significantly determines the effectiveness of SLA. Conflicting policies can be downright damaging to the autonomic system. The paper describes how a formal technique termed model checking can be used to detect conflicts (reveal SLA violations) in autonomic-component ensembles (ACE).