Formalization and Verification of Behavioral Correctness of Dynamic Software Updates
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates
复制标题
DOI：
10.1016/j.entcs.2013.02.013
复制
发表时间：
2013-03
期刊：
影响因子：
--
通讯作者：
Min Zhang;K. Ogata;K. Futatsugi
中科院分区：
文献类型：
--
作者：
Min Zhang;K. Ogata;K. Futatsugi
动态软件更新(DSU)是一种动态更新正在运行的软件系统的技术。虽然有一些关于动态更新的正确性的研究，但他们关注的是如何在代码级别正确地部署更新，例如，如果过程引用了正确类型的数据。然而，很少有人关注行为级别的动态更新的正确性，例如，系统在更新后是否按预期运行，以及是否永远不会发生意外行为。我们提出了一种代数方法，通过使用现成的定理证明和模型检测工具来指定动态更新并验证其行为正确性。通过定理证明，我们可以证明更新后的系统确实满足其期望的性质，并且通过模型检验，我们可以检测潜在的错误。我们的方法是通用的：(1)它可以应用于当前DSU系统中主要使用的三种更新模型；(2)它不限于对某些编程模型的动态更新。
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.