Towards Verifying Global Properties of Adaptive Software Based on Linear Temporal Logic

Increasingly, software needs to dynamically adapt its structure and behavior at runtime in response to changing conditions in the supporting computing, network infrastructure, and in the surrounding physical environments. By high complexity, assurance of high dependability of these software is a great challenge. Effective modeling of behavior and flexibly specifying requirements are the key issues for developing trusted adaptive software. This paper introduces a formal model for the behavior of adaptive software and an extended linear temporal logic to specify global properties. We use state machines to describe programs in different behavioral modes of adaptive software and consider these machines as different versions of programs. Specifications are classified into three categories, local, adaptation and global properties from perspective of dynamic adaptation. To specify and verify global properties on our model, we propose the versioned LTL (vLTL) which extends Linear Temporal Logic by adding version related element and enables describing properties on different versions. We also discuss verifying approach of vLTL by transforming them into LTL formulae and illustrate a study case.