Formalizing consistent dynamic updates for component-based software

To enable the updated system to run correctly, it is very important to reason about some meaning and possible effects of updates. In this paper, we propose a formal calculus update π, a variant extension of higher-order π calculus, to model dynamic updates of component-based software, which is language and technology independent. This calculus focuses on some main aspects which include granularity of update, timing of update, state transformation and update failure recovery. Some applications of this formal method to those general dynamic update processes and the relational analysis of property and verification show that the update π calculus can reasonably reason about and ensure the safety and consistency of dynamic updates.