Model-based development of dynamically adaptive software

TLDR

Software increasingly must dynamically adapt at run‑time to changing computing, communication, and physical environments, yet adaptive programs are more difficult to specify, verify, and validate—especially with multi‑threaded adaptations—making trust in their correct functioning during and after adaptations essential. This paper introduces an approach to create formal models for the behavior of adaptive programs. Our approach separates adaptation and non‑adaptive behavior specifications, introduces a process to construct adaptation models, automatically generates adaptive programs from the models, and verifies and validates them. The approach is illustrated by developing an adaptive GSM‑oriented audio streaming protocol for a mobile computing application.

Abstract

Increasingly, software should dynamically adapt its behavior at run-time in response to changing conditions in the supporting computing and communication infrastructure, and in the surrounding physical environment. In order for an adaptive program to be trusted, it is important to have mechanisms to ensure that the program functions correctly during and after adaptations. Adaptive programs are generally more difficult to specify, verify, and validate due to their high complexity. Particularly, when involving multi-threaded adaptations, the program behavior is the result of the collaborative behavior of multiple threads and software components. This paper introduces an approach to create formal models for the behavior of adaptive programs. Our approach separates the adaptation behavior and non-adaptive behavior specifications of adaptive programs, making the models easier to specify and more amenable to automated analysis and visual inspection. We introduce a process to construct adaptation models, automatically generate adaptive programs from the models, and verify and validate the models. We illustrate our approach through the development of an adaptive GSM-oriented audio streaming protocol for a mobile computing application.