Controller synthesis of service contracts with variability

Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one.