An algebraic approach to formal analysis of dynamic software updating mechanisms

Dynamic Software Updating (DSU) is a promising software maintenance technique, which aims at updating running software systems on the fly without incurring any downtime. The systems that require dynamic updating usually require high reliability assurance. Incorrect updating may cause them to behave erratically and/or even crash, and hence results in dreadful loss. However, there are few approaches to the study of the correctness of dynamic updating. In this paper, we systematically discuss the correctness of dynamic updating from a formal perspective, and present a first algebraic approach to formal analysis of it. The basic idea is to formalize dynamic updating systems as rewrite systems, with which we can analyze dynamic updates e.g. verifying their desired properties, or detecting incorrect update points, etc. The formal analysis helps us understand the behaviors of updated systems before we apply updates to the running systems, and hence improves the reliability of the systems after being updated.