Title :
Formal reasoning about runtime code update
Author :
Charlton, Nathaniel ; Horsfall, Ben ; Reus, Bernhard
Author_Institution :
Sch. of Inf., Univ. of Sussex, Brighton, UK
Abstract :
We show how dynamic software updates can be modelled using a “higher order store” programming language where procedures can be written to the heap. We then show how such updates can be proved correct with a Hoare-calculus that allows for keeping track of behavioural specifications of such stored procedures.
Keywords :
programming languages; software engineering; Hoare-calculus; behavioural specification; dynamic software update; formal reasoning; programming language; runtime code update; Calculus; Computer crashes; Loading; Runtime; Semantics; Servers; Software;
Conference_Titel :
Data Engineering Workshops (ICDEW), 2011 IEEE 27th International Conference on
Conference_Location :
Hannover
Print_ISBN :
978-1-4244-9195-7
Electronic_ISBN :
978-1-4244-9194-0
DOI :
10.1109/ICDEW.2011.5767624
