Verifying the design of dynamic software updating in the OTS/CafeOBJ method

被引：2

作者：

Zhang, Min ^{[1
]}

Ogata, Kazuhiro ^{[1
]}

Futatsugi, Kokichi ^{[1
]}

机构：

[1] Research Center for Software Verification, Japan Advanced Institute of Science and Technology (JAIST)

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8373卷

关键词：

D O I：

10.1007/978-3-642-54624-2_28

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

Dynamic Software Updating (DSU) is a technique for updating running software systems without incurring downtime. However, a challenging problem is how to design a correct dynamic update so that the system after being updated will run as expected instead of causing any inconsistencies or even crashes. The OTS/CafeOBJ method is an effective and practical approach to specifying and verifying the design of software. In this paper, we propose an algebraic way of specifying and verifying the design of dynamic updates in the OTS/CafeOBJ method. By verifying the design of a dynamic update, we can (1) gain a better understanding of the update, e.g., how the behavior of the running system is affected by the update, (2) identify updating points where the dynamic update can be safely applied, (3) detect potential errors, and hence (4) design a safer dynamic update. © 2014 Springer-Verlag Berlin Heidelberg.

引用

页码：560 / 577

页数：17

共 27 条

[1]

Hicks M., Nettles S., Dynamic software updating, ACM TOPLAS, 27, pp. 1049-1096, (2005)

[2]

Duggan D., Type-based hot swapping of running modules, In Functional Programming, 36, pp. 62-73, (2001)

[3]

Stoyle G., Hicks M., Bierman G., Et al., Mutatis mutandis: Safe and predictable dynamic software updating, ACM TOPLAS, 40, pp. 183-194, (2005)

[4]

Neamtiu I., Hicks M., Foster J., Et al., Contextual effects for version-consistent dynamic software updating and safe concurrent programming, In POPL, 43, pp. 37-49, (2008)

[5]

Gupta D., Jalote P., Barua G., A formal framework for on-line software version change, IEEE Transactions on Software Engineering, 22, 2, pp. 120-131, (1996)

[6]

Hayden C.M., Magill S., Hicks M., Foster N., Foster J.S., Specifying and verifying the correctness of dynamic software updates, LNCS, 7152, pp. 278-293, (2012)

[7]

Zhang M., Ogata K., Futatsugi K., Formalization and verification of behavioral correctness of dynamic software updates, Electr. Notes Theor. Comput. Sci., 294, pp. 12-23, (2013)

[8]

Futatsugi K., Goguen J.A., Ogata K., Verifying design with proof scores, LNCS, 4171, pp. 277-290, (2008)

[9]

Ogata K., Futatsugi K., Proof scores in the OTS/CafeOBJ method, LNCS, 2884, pp. 170-184, (2003)

[10]

Ogata K., Futatsugi K., Compositionally writing proof scores of invariants in the OTS/CafeOBJ method, J. UCS, 19, pp. 771-804, (2013)

← 1 2 3 →