@inproceedings{7f7924c3605848b28686309316a05bf0,
title = "Towards a formal approach to modeling and verifying the design of dynamic software updates",
abstract = "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.",
keywords = "Design, Dynamic Software Updating, Formal Verification, Maude, Model checking",
author = "Min Zhang and Kazuhiro Ogata and Kokichi Futatsugi",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 22nd Asia-Pacific Software Engineering Conference, APSEC 2015 ; Conference date: 01-12-2015 Through 04-12-2015",
year = "2016",
month = may,
day = "9",
doi = "10.1109/APSEC.2015.28",
language = "英语",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "159--166",
editor = "Jing Sun and Reddy, \{Y. Raghu\} and Arun Bahulkar and Anjaneyulu Pasala",
booktitle = "Proceedings - 22nd Asia-Pacific Software Engineering Conference, APSEC 2015",
address = "美国",
}