TY - GEN
T1 - TRAC
T2 - 26th International Conference on Coordination Models and Languages, COORDINATION 2024
AU - Afonso, João
AU - Konjoh Selabi, Elvis
AU - Murgia, Maurizio
AU - Ravara, António
AU - Tuosto, Emilio
N1 - info:eu-repo/grantAgreement/EC/H2020/778233/EU#
info:eu-repo/grantAgreement/FCT/Concurso de avaliação no âmbito do Programa Plurianual de Financiamento de Unidades de I&D (2017%2F2018) - Financiamento Base/UIDB%2F04516%2F2020/PT#
info:eu-repo/grantAgreement/FCT/3599-PPCDT/2022.09138.PTDC/PT#
Funding Information:
Research partly supported by the PRIN 2022 PNRR project DeLiCE (F53D23009130001), by the MUR project PON REACT EU DM 1062/21, by the PRO3 MUR project Software Quality, \u201Cby the MUR dipartimento di eccellenza\u201D, and by PNRR MUR project VITALITY (ECS00000041), Spoke 2 ASTRA - Advanced Space Technologies and Research Alliance.
Publisher Copyright:
© IFIP International Federation for Information Processing 2024.
PY - 2024/6
Y1 - 2024/6
N2 - We propose , a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, can specify the coordination of the participants of a distributed protocol for instance an execution model akin blockchain smart contracts (SCs). In fact, the transitions of our FSMs yield guards, and assignments over data variables, and with participants binders. The latter allow us to model scenarios with an unbounded number of participants which can vary at run-time. We introduce a notion of well-formedness to rule out meaningless or problematic specifications. This notion is verified with and demonstrated on several case studies borrowed from the smart contracts domain. Then, we evaluate the performance of using a set of randomised examples, studying the correlations between the features supported and the time taken to decide well-formedness.
AB - We propose , a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, can specify the coordination of the participants of a distributed protocol for instance an execution model akin blockchain smart contracts (SCs). In fact, the transitions of our FSMs yield guards, and assignments over data variables, and with participants binders. The latter allow us to model scenarios with an unbounded number of participants which can vary at run-time. We introduce a notion of well-formedness to rule out meaningless or problematic specifications. This notion is verified with and demonstrated on several case studies borrowed from the smart contracts domain. Then, we evaluate the performance of using a set of randomised examples, studying the correlations between the features supported and the time taken to decide well-formedness.
UR - http://www.scopus.com/inward/record.url?scp=85197269998&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-62697-5_13
DO - 10.1007/978-3-031-62697-5_13
M3 - Conference contribution
AN - SCOPUS:85197269998
SN - 978-3-031-62696-8
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 239
EP - 257
BT - Coordination Models and Languages
A2 - Castellani, Ilaria
A2 - Tiezzi, Francesco
PB - Springer
CY - Cham
Y2 - 18 June 2024 through 20 June 2024
ER -