Towards a formal model for composable container systems


In modern cloud-based architectures, containers play a central role: they provide powerful isolation mechanisms such that developers can focus on the logic and dependencies of applications while system administrators can focus on deployment and management issue. We propose a formal model for container-based systems, using the framework of Bigraphical Reactive Systems (BRSs). These graphs can be analysed and manipulated using techniques from graph theory: properties about containers can be formalized as properties of the corresponding bigraphic representations. Moreover, it turns out that the composition of containers as performed by e.g. docker-compose, corresponds precisely to the composition of the corresponding bigraphs inside an “environment bigraph” which in turn is obtained directly from the YAML file used to define the composition of containers.