Abstract
The microservice architectural style is often used to implement modern cloud, IoT, and large-scale distributed applications. Here software development processes are characterized by short incremental iterations, where several updates and new functionalities are continuously integrated many times a day in a agile fashion. Such a paradigm shift calls for new formal approaches to systematic (design-time and runtime) verification. This paper introduces a formal framework to apply continuous verification of microservice based applications built on top of Conductor, i.e., an open source orchestration engine of microservices workflows in use at Netflix, Inc. for their production environment. Our proposal adopts a model-driven paradigm and it leverages solid foundation from Petri nets to specify and verify the behavior of time-dependent workflows. This paper describes our approach, the current implementation, and evaluation activity conducted on a taxi-hailing application example