%0 Conference Proceedings
%T Supervisory Synthesis of Configurable Behavioural Contracts with Modalities
%+ CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” [Pisa] (CNR | ISTI)
%+ University of Pisa - Università di Pisa
%+ Université Catholique de Louvain = Catholic University of Louvain (UCL)
%A Basile, Davide
%A Beek, Maurice
%A Degano, Pierpaolo
%A Legay, Axel
%A Ferrari, Gian-Luigi
%A Gnesi, Stefania
%A Giandomenico, Felicita, Di
%Z Part 2: Short and Journal-First Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Valletta, Malta
%Y Kirstin Peters
%Y Tim A.C. Willemse
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-12719
%P 177-181
%8 2021-06-14
%D 2021
%R 10.1007/978-3-030-78089-0_10
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Service contracts characterise the desired behavioural compliance of a composition of services, typically defined by the fulfilment of all service requests through service offers. Contract automata are a formalism for specifying behavioural 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. This short paper summarises the contributions published in [8], where we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded; and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A recently redesigned and refactored tool supports the developed theory.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03740267/document
%2 https://inria.hal.science/hal-03740267/file/509782_1_En_10_Chapter.pdf
%L hal-03740267
%U https://inria.hal.science/hal-03740267
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-12719