2015 Asia-Pacific Software Engineering Conference (APSEC) (2015)
New Delhi, India
Dec. 1, 2015 to Dec. 4, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.2015.28
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. One of the challenges of designing a correct dynamic update is to identify a set of update points where the update can be safely applied to a running system. In this paper, we present a formal approach to modeling dynamic software updates and use the formal model to identify safe update points. In our approach, we formalize dynamic updates as state machines, and verify by model checking a set of desired properties which the running system is expected to satisfy after being updated. If counterexamples are found, we exclude those states that cause the counterexamples, and do model checking again. The process is iterated until all desired properties are successfully verified. We then finally obtain a set of safe update points. A case study is also presented to demonstrate the feasibility of the proposed approach.
Synchronization, Software systems, Model checking, Computational modeling, Instruction sets, Electronic mail
M. Zhang, K. Ogata and K. Futatsugi, "Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates," 2015 Asia-Pacific Software Engineering Conference (APSEC), New Delhi, India, 2016, pp. 159-166.