%0 Conference Proceedings
%T Playing with Our CAT and Communication-Centric Applications
%+ CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” [Pisa] (CNR | ISTI)
%+ University of Pisa - Università di Pisa
%+ University of Leicester
%A Basile, Davide
%A Degano, Pierpaolo
%A Ferrari, Gian-Luigi
%A Tuosto, Emilio
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 62-73
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_5
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432928/document
%2 https://inria.hal.science/hal-01432928/file/426757_1_En_5_Chapter.pdf
%L hal-01432928
%U https://inria.hal.science/hal-01432928
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688