SLAFM: A service level agreement formal model for Cloud Computing

Cloud Computing services are regulated by a contract called Service Level Agreement (SLA). It is co-signed between the customers and the providers after a negotiation phase, and during their validity time several constraints have to be respected by the involved parties. Due to their popularity, cloud services are enormously used and unfortunately also abused, specially by cyber-criminals. Sometimes the crimes have the consequence of violating some contractual constraints without the parties are aware of. A manner for guaranteeing more control of the SLA respect is to consider a dedicated system interacting with the cloud services and detecting the SLA violations by analysing the log files. We introduce a formal model aimed to represent the contents of such SLAs necessary in the context of an automatic mechanism for detecting SLA violations