Formal reasoning about runtime code update

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...

Full description

Saved in:
Bibliographic Details
Main Authors: Charlton, N, Horsfall, B, Reus, B
Format: Conference Proceeding
Language:English
Subjects:
Calculus
Computer crashes
Loading
Runtime
Semantics
Servers
Software
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/ICDEW.2011.5767624