|
JAIST Repository >
School of Information Science >
Articles >
Journal Articles >
Please use this identifier to cite or link to this item:
https://hdl.handle.net/10119/12218
|
| Title: | Formalization and Verification of Behavioral Correctness of Dynamic Software Updates |
| Authors: | Zhang, Min
Ogata, Kazuhiro
Futatsugi, Kokichi |
| Keywords: | dynamic software updating
algebraic specification
verification
behavioral property |
| Issue Date: | 2013-03-15 |
| Publisher: | Elsevier |
| Magazine name: | Electronic Notes in Theoretical Computer Science |
| Volume: | 294 |
| Start page: | 12 |
| End page: | 23 |
| DOI: | 10.1016/j.entcs.2013.02.013 |
| Abstract: | Dynamic Software Updating (DSU) is a technique of updating running software systems on-the-fly. Whereas there are some studies on the correctness of dynamic updating, they focus on how to deploy updates correctly at the code level, e.g., if procedures refer to the data of correct types. However, little attention has been paid to the correctness of the dynamic updating at the behavior level, e.g., if systems after being updated behave as expected, and if unexpected behaviors can never occur. We present an algebraic methodology of specifying dynamic updates and verifying their behavioral correctness by using off-the-shelf theorem proving and model checking tools. By theorem proving we can show that systems after being updated indeed satisfy their desired properties, and by model checking we can detect potential errors. Our methodology is general in that: (1) it can be applied to three updating models that are mainly used in current DSU systems; and (2) it is not restricted to dynamic updates for certain programming models. |
| Rights: | © 2013 Elsevier B.V. Open access under CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/3.0/). Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi, Electronic Notes in Theoretical Computer Science, 294, 2013, 12-23, http://dx.doi.org/10.1016/j.entcs.2013.02.013 |
| URI: | https://hdl.handle.net/10119/12218 |
| Material Type: | publisher |
| Appears in Collections: | b10-1. 雑誌掲載論文 (Journal Articles)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 19812.pdf | | 288Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
