A Formal Framework for Component Deployment

Research Paper

Thursday, Oct 26, from 13:30 to 15:00

Software deployment is a complex process, and industrial-strength frameworks such as .NET, Java, and CORBA all provide explicit support for component deployment. However, these frameworks are not built around fundamental principles as much as they are engineering efforts closely tied to particulars of the respective systems. Here we aim to elucidate the fundamental principles of software deployment, in a platform-independent manner. Issues that need to be addressed include deployment unit design, when, where and how to wire components together, versioning, version dependencies, and hot-deployment of components. We define the application buildbox as the place where software is developed and deployed, and define a formal Labelled Transition System (LTS) on the buildbox with transitions for deployment operations that include build, install, ship, and update. We establish formal properties of the LTS, including the fact that built components which meet their dependency constraints can always be executed. Our treatment of deployment is both platform- and vendor-independent, and we show how it models the core mechanisms of the industrial-strength deployment frameworks.