Timed service contract automata

Weequiparecentlydevelopedmodelforthespecification of service contracts with real-time constraints. Service contracts offer a means to define the behavioural compliance of a composition of services, typically dictated in a Service-Level Agreement (SLA), as the fulfilment of all service requests through service offers. Depending on their granularity,SLAsvaryaccordingtothelevelofcriticalityof theinvolvedservicesandalsocontainreal-timeaspects,like theservices’responseorexpirationtime.Astandardmethod to refine a spurious service composition into a compliant one is via the synthesis of a safe orchestration, in the form of the most permissive controller from Supervisory Control Theory(SCT).Ideally,safeorchestrationssolvecompetition amongmatchingservicerequestsandoffers,inlightoftheir criticalities and their timing constraints, in the best possible way. In this paper, we introduce timed service contract automata as a novel formal model for service contracts with real-time constraints on top of services with varying levels of criticality. We also define a means to efficiently compute theircompositionandtheirsafeorchestration,usingtheconcept of zones from timed games. The innovations of our contribution are illustrated by intuitive examples and by a preliminary evaluation