Dynamic software updating (DSU) enables running programs to be updated with
new code and data without interrupting their execution. A number of DSU
systems have been designed, but there is still little rigorous understanding
of how to use DSU technology so that updates are safe. As a first step in
this direction, we introduce a small *update calculus* with a precise
mathematical semantics. The calculus is formulated as an extension of a
typed lambda calculus, and supports updating technology similar to
that of the programming language Erlang. Our goal
is to provide a simple yet expressive foundation for reasoning about
dynamically updateable software. In this paper, we present the details of
the calculus, give some examples of its expressive power, and discuss how
it might be used or extended to guarantee safety properties.

[ .pdf ]

@INPROCEEDINGS{BiermanHSS03, AUTHOR = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle}, TITLE = {Formalizing Dynamic Software Updating}, BOOKTITLE = {On-line Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE)}, MONTH = {April}, YEAR = {2003}, NOTE = {\url{http://www.informatik.uni-bonn.de/~gk/use/2003/Papers/papers.html}} }