We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our main motivation is to establish a framework for the comparison and generalisation of standard constructions and properties from the literature. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. A condition is also devised to guarantee relevant communication properties such as (dead)lock-freedom. Formal choreographic languages capture existing formalisms for message-passing systems; we detail the cases of multiparty session types and choreography automata. Unlike many other models, formal choreographic languages can naturally model systems exhibiting non-regular behaviour.
Formal Choreographic Languages / Barbanera F.; Lanese I.; Tuosto E.. - STAMPA. - 13271:(2022), pp. 121-139. (Intervento presentato al convegno COORDINATION tenutosi a Lucca nel 14-16/6/2022) [10.1007/978-3-031-08143-9_8].
Formal Choreographic Languages
Lanese I.;
2022
Abstract
We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our main motivation is to establish a framework for the comparison and generalisation of standard constructions and properties from the literature. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. A condition is also devised to guarantee relevant communication properties such as (dead)lock-freedom. Formal choreographic languages capture existing formalisms for message-passing systems; we detail the cases of multiparty session types and choreography automata. Unlike many other models, formal choreographic languages can naturally model systems exhibiting non-regular behaviour.File | Dimensione | Formato | |
---|---|---|---|
main.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per accesso libero gratuito
Dimensione
634.22 kB
Formato
Adobe PDF
|
634.22 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.