PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Basile D., Degano P., Ferrari G., Tuosto E. Playing with our CAT and Communication-Centric Applications. In: FORTE 2016 - Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference (Heraklion, Crete, Greece, 6-9 June 2016). Proceedings, pp. 62 - 73. Elvira Albert, Ivan Lanese (eds.). (Lecture Notes in Computer Science, vol. 9688). Springer International Publishing, 2016.
 
 
Abstract
(English)
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. The first three authors have been partially supported by project PRA_2016_64 "Through the fog" funded by the University of Pisa.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-39570-8_5
DOI: 10.1007/978-3-319-39570-8_5
Subject Formal Verification
Tool
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification


Icona documento 1) Download Document PDF
Icona documento 2) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional