Preventing Performance Violations of Service Compositions Using Assumption-Based Run-Time Verification

Service-based Applications (SBAs) will increasingly be deployed in highly distributed and dynamic settings. To a large extent this dynamicity is caused by the trend to increasingly compose SBAs using third-party services. Those services are provided by external organizations and are thus not under the control of the SBA provider. For critical application domains (such as emergency or financial) and important customers (such as key accounts), the SBA developer needs to ensure that each individual SBA instance will live up to its expected requirements even though its constituent, third-party services might fail. To prevent such requirements violations, SBAs should be equipped with monitoring, prediction and adaptation capabilities which are able to foresee and avert menacing violations. Several approaches exploiting preventive adaptations have been presented in the literature, but they rely on the existence of cost models or comprehensive training data that limit their applicability in practice. In this paper we present SPADE, an automated technique that addresses those limitations. Based on assumptions about the SBA’s constituent services (derived from SLAs), SPADE formally verifies the SBA against its requirements during run-time. The experimental evaluation of SPADE, using data collected for six real services, demonstrates its practical applicability in predicting violations of performance requirements.