Formalisation and Static Analysis for the Serverless Choreographic Programming Language FaaSChal

Modern computing relies more than ever on two aspects: concurrency, the performance of multiple tasks at the same time; and distribution, the usage of components located on different communicating devices. This is due to the rising importance of the World Wide Web, the Internet of Things, and telecommunications, and due to the rising popularity of edge computing and cloud computing, all of which lead to larger computer networks. Cloud computing in particular is one of the main environments where distributed systems run, since it allows for greater scalability and easier management of resources. One of the main design approaches used with cloud computing is serverless computing, which consists of defining functions with specific triggers, letting the cloud provider handle their instantiation when they are triggered. For these reasons, a new programming language, called FaaSChal, was proposed, with the aim of making it easier for programmers to specify the behaviour of serverless systems, and of guaranteeing freedom from certain types of communication errors. FaaSChal is a choreographic language, meaning that the behaviour of all processes that participate in the system is specified in a single program. In this thesis we formalize a choreographic calculus, called FaaSChalCore, which contains all the key features of FaaSChal, and we define a static analysis discipline that, by separating correct and incorrect programs, allows us to prove important properties for the language on the correct programs, like guaranteeing that serverless functions terminate properly before the system ends execution.