The microservices architectural style is inspired by serviceoriented computing and has recently started to gain in popularity. This novel approach is changing the way in which software is perceived, conceived and designed. Thus, there is a call for techniques and tools supporting the problem of specifying and verifying communication behavior of microservice systems. We present a formal semantics based on Petri nets for microservices based process flows specified using the Conductor orchestration language: a JSON domain specific language designed by Netflix, Inc. We give a formal semantics in terms of a translation from Conductor specifications into Time Basic Petri net models, i.e., Petri nets supporting the definition of temporal constraints. The Petri net model can be used for computer aided verification purposes by means of well-known techniques implemented by powerful, off-the-shelf model checking tools.
A Formal Framework for Specifying and Verifying Microservices Based Process Flows / M. Camilli, C. Bellettini, L. Capra, M. Monga - In: Software Engineering and Formal Methods / [a cura di] A. Cerone, M. Roveri. - [s.l] : Springer International Publishing, 2018. - ISBN 9783319747804. - pp. 187-202 (( convegno Microservices: Science and Engineering tenutosi a Trento nel 2017.
A Formal Framework for Specifying and Verifying Microservices Based Process Flows
M. Camilli
;C. Bellettini;L. Capra;M. Monga
2018
Abstract
The microservices architectural style is inspired by serviceoriented computing and has recently started to gain in popularity. This novel approach is changing the way in which software is perceived, conceived and designed. Thus, there is a call for techniques and tools supporting the problem of specifying and verifying communication behavior of microservice systems. We present a formal semantics based on Petri nets for microservices based process flows specified using the Conductor orchestration language: a JSON domain specific language designed by Netflix, Inc. We give a formal semantics in terms of a translation from Conductor specifications into Time Basic Petri net models, i.e., Petri nets supporting the definition of temporal constraints. The Petri net model can be used for computer aided verification purposes by means of well-known techniques implemented by powerful, off-the-shelf model checking tools.File | Dimensione | Formato | |
---|---|---|---|
mse17.pdf
accesso riservato
Descrizione: Articolo
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
784.55 kB
Formato
Adobe PDF
|
784.55 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.