A Formal Model for Supporting Frameworks of Dynamic Service Update Based on OSGi

Author

Chen, Junqing ; Huang, Linpeng ; Du, Siqi ; Zhou, Wenjia

Author_Institution

Dept. of Comput. Sci. & Eng., Shanghai Jiao Tong Univ., Shanghai, China

fYear

2010

fDate

Nov. 30 2010-Dec. 3 2010

Firstpage

234

Lastpage

241

Abstract

The continuous requirements of evolving a service-oriented application and the rising cost of shutting down services at runtime are forcing researchers to find ways of updating services while they run. Dynamic service update can solve the problem of such applications and is becoming a challenging issue. This paper presents a formal model for supporting dynamic update framework based on OSGi. The process of dynamic service update is specified using Finite State Process (FSP) and then the Labelled Transition System Analyzer (LTSA) tool for formal property verifications. We also formally analyze and prove type-safe update of such frameworks, and finally demonstrate that our model works well in practical cases.

Keywords

formal verification; service-oriented architecture; ubiquitous computing; OSGi; dynamic service update; finite state process; formal property verifications; labelled transition system analyzer; service-oriented application; Analytical models; Process control; Runtime; Safety; Servers; Synchronization; System recovery; FSP; OSGi; dynamic service update; service-oriented application; type safety;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference (APSEC), 2010 17th Asia Pacific

Conference_Location

Sydney, NSW

ISSN

1530-1362

Print_ISBN

978-1-4244-8831-5

Electronic_ISBN

1530-1362

Type

conf

DOI

10.1109/APSEC.2010.35

Filename

5693199