Document - Playing with our CAT and communication-centric applications

2016

Conference article Open Access

Playing with our CAT and communication-centric applications

Basile D., Degano P., Ferrari G. -L., Tuosto E.

[ INFO.INFO-NI ] Computer Science [cs]/Networking and Internet Architecture [cs.NI] Formal Verification [ INFO ] Computer Science [cs] D.2.4 SOFTWARE ENGINEERING. Software/Program Verification Tool

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.

Source: Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference, pp. 62–73, Heraklion, Crete, Greece, 6-9 June 2016

Publisher: Springer, Berlin , Germania

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:362669,
	title = {Playing with our CAT and communication-centric applications},
	author = {Basile D. and Degano P. and Ferrari G. -L. and Tuosto E.},
	publisher = {Springer, Berlin , Germania},
	doi = {10.1007/978-3-319-39570-8_5},
	booktitle = {Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference, pp. 62–73, Heraklion, Crete, Greece, 6-9 June 2016},
	year = {2016}
}