Counterexample-guided Design of Property-based Dynamic Software Updates

• Zhang Min

Even though software systems in some domains are expected to provide continuous services, most of them must undergo some form of changes. It leads to the emergence of dynamic software updating, a technique for updating a running software system without incurring any downtime. Several dynamic updating approaches, focusing on how programs and binary code are altered in memory, have been proposed. But little attention has been given to the methodologies of designing intended dynamic updates so that the systems after being updated will satisfy the desired properties.

In this talk, we will introduce a novel counterexample-guided approach to designing intended dynamic updates by identifying safe update points and defining correct state transformation function. In our approach, we formalize dynamic updates as state machines, and verify their correctness by model checking a set of desired properties which should be satisfied by the system after being updated. Guided by the counterexamples that are found by model checking, we can finally identify a set of update points and refine a state transformation function until all the properties are successfully verified.

Attachment	Size
ZhangMin.pdf	769.54 KB