A Full Operational Semantics for Asynchronous Relational Networks

VISSANI, IGNACIO; LOPEZ POMBO, CARLOS GUSTAVO; TUTU, IONUT; FIADEIRO, JOSÉ LUIZ

LECTURE NOTES IN COMPUTER SCIENCE

Springer-Verlag

Lugar: Berlín; Año: 2015 vol. 9463 p. 131 - 150

0302-9743

Service-oriented computing is a new paradigm where appli- cations run over global computational networks and are formed by ser- vices discovered and bound at run-time through the intervention of a middleware. Asynchronous Relational Nets (ARNs) were presented by Fiadeiro and Lopes with the aim of formalising the elements of an in- terface theory for service-oriented software designs. The semantics of ARNs was originally given in terms of sequences of sets of actions cor- responding to the behaviour of the service. Later, they were given an institution-based semantics where signatures are ARNs and models are morphisms into ground networks, that have no dependencies on external services. In this work, we propose a full operational semantics capable of reflecting the dynamic nature of service execution by making explicit the reconfig- urations that take place at run-time as the result of the discovery and binding of required services. This provides us a refined view of the execu- tion of ARNs based upon which a specialized variant of linear temporal logic can be used to express, and even to verify through standard model- checking techniques, properties concerning the behaviour of ARNs that are more complex than those considered before.