A Formal Framework for Specifying and Verifying Microservices Based Process Flows

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.