Formalizing dynamic software updating

TitleFormalizing dynamic software updating
Publication TypeJournal Articles
Year of Publication2003
AuthorsBierman G, Hicks MW, Sewell P, Stoyle G
JournalProceedings of the Second International Workshop on Unanticipated Software Evolution (USE)
Date Published2003///
Abstract

Dynamic software updating (DSU) enables running programs to beupdated with new code and data without interrupting their execution. A
number of DSU systems have been designed, but there is still little rig-
orous 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 [2]. Our goal is to
provide a simple yet expressive foundation for reasoning about dynam-
ically 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.