An Event-Based Formal Framework For Dynamic Software Update

Software updates are inevitable. Normally, these updates are applied to a produc-tion system through three steps:shutting down the system, installing new-version pro-gram and restarting the system. However, this kind of offline updates are unacceptable in some circumstances where non-stopping services are mandatory, such as financial transaction processing and transport controlling. Besides, the disruptions caused by frequent offline updates can be annoying for everyday software applications. Dynamic software update (DSU) is a technique to upgrade a running program to a new version on the fly.However, DSU has been rarely used in real-world practice, mainly because there is a risk that DSU may cause misbehaviors that would never present in either the old or the new version of the program. To manage the risk, various formal models have been proposed for the specification and verification of DSU. However, some of them, are too loose to ensure the safety of DSU. Others tend to cause over-specification, because they take an operational view of DSU, and one must explicitly specify what kind of cross-version program trace is allowed. To address those shortcomings, we propose a new formal framework. The intended contributions of this dissertation are as follows.1. We propose a formal framework to define DSU and its correctness using LTS and FLTL. The framework helps avoid over-specification of DSU and allows for better DSU flexibility, thanks to its event-based specification and explicit environment modeling.2. We derive a runtime monitoring mechanism to improve the timeliness of DSU with-out compromising its safety. Different from the conservative approach that only considers static analyses, we take runtime information into consideration to im- prove the updatabilty. We also provide an algorithm to generate the monitor auto-matically.3. We define the smoothness of DSU as a criterion to analyse the quality of DSU. A DSU is smooth, if the update preserves the valuable computed results. This can help us to avoid the high cost of redoing or recovery.