A formal approach for Docker container deployment

Container-based virtualization is becoming increasingly popular in the cloud industry, as it provides services to the client as per their requirements. Requirements of the user can be described in a configuration file. Cloud provider offers the services to the client using "pay-as-you go" model. Docker provides support to a cloud provider for the creation of a container, deployment of the container, and monitoring of services running inside a container on the host and guest system both. The creation and deployment of the container by Docker efficiently is a big challenge. In this paper, we capture the behavior of the container life cycle through process algebra (CCS) and properties of it as a formula using mu-calculus. Further we capture the behavior of deployment of the container on the host machine through CCS and its properties through the model mu- calculus. We used model checking tool Concurrency Workbench of the New Century to verify the creation of the Docker container as well as deployment of it.