Controller synthesis of contract-based service product lines: extended version

In Service-Oriented Computing, contracts offer a way to characterise the behavioural conformance of a composition of services, and guarantee that the results do not lead to spurious compositions. Through variability modelling, a product line of services is enabled to adapt to customer requirements and to changes in the context where they operate. We extend a previously introduced formal model of service contracts towards variability and product line modelling, in particular we include: (i) feature-based constraints and (ii) four classes of service requests to characterise different types of service agreement. We then exploit Supervisory Control Theory to synthesise the most permissive controller of a composition of services that satisfies: (i) all feature constraints of the service product line, and (ii) the maximal number of service requests for which an agreement can be reached. Moreover, the controller of a service product line, whose number of products is potentially exponential in the number of features, can be synthesised from only a subset of its products. A prototypical tool supports the developed theory.