Formalizing Event-Driven Behavior of Serverless Applications
This work addresses the need for formal modeling of serverless computing interactions, which is incremental in providing tools for analysis and debugging.
The authors tackled the problem of modeling event-driven behavior in serverless applications by developing new operational semantics and a service call graph concept, and they evaluated accuracy on twelve JavaScript applications.
We present new operational semantics for serverless computing that model the event-driven relationships between serverless functions, as well as their interaction with platforms services such as databases and object stores. These semantics precisely encapsulate how control transfers between functions, both directly and through reads and writes to platform services. We use these semantics to define the notion of the service call graph for serverless applications that captures program flows through functions and services. Finally, we construct service call graphs for twelve serverless JavaScript applications, using a prototype of our call graph construction algorithm, and we evaluate their accuracy.