A Formal Model for Dynamically Adaptable Services

TL;DR

This paper introduces a formal model for dynamic adaptation in service-oriented systems, addressing the complexity and need for correctness, reliability, and responsiveness in adaptable, heterogeneous environments.

Contribution

It presents a formal, COWS-based model and theory for dynamic adaptation, enabling verification of system properties like reliability and responsiveness.

Findings

Model verified with CMC for reliability

Ensures correctness of dynamic adaptations

Addresses heterogeneity and real-time constraints

Abstract

The growing complexity of software systems as well as changing conditions in their operating environment demand systems that are more flexible, adaptive and dependable. The service-oriented computing paradigm is in widespread use to support such adaptive systems, and, in many domains, adaptations may occur dynamically and in real time. In addition, services from heterogeneous, possibly unknown sources may be used. This motivates a need to ensure the correct behaviour of the adapted systems, and its continuing compliance to time bounds and other QoS properties. The complexity of dynamic adaptation (DA) is significant, but currently not well understood or formally specified. This paper elaborates a well-founded model and theory of DA, introducing formalisms written using COWS. The model is evaluated for reliability and responsiveness properties with the model checker CMC.