Amir Molzam Sharifloo

Pooyan Jamshidi, Amir Sharifloo, Claus Pahl et al.

Cloud controllers aim at responding to application demands by automatically scaling the compute resources at runtime to meet performance guarantees and minimize resource costs. Existing cloud controllers often resort to scaling strategies that are codified as a set of adaptation rules. However, for a cloud provider, applications running on top of the cloud infrastructure are more or less black-boxes, making it difficult at design time to define optimal or pre-emptive adaptation rules. Thus, the burden of taking adaptation decisions often is delegated to the cloud application. Yet, in most cases, application developers in turn have limited knowledge of the cloud infrastructure. In this paper, we propose learning adaptation rules during runtime. To this end, we introduce FQL4KE, a self-learning fuzzy cloud controller. In particular, FQL4KE learns and modifies fuzzy rules at runtime. The benefit is that for designing cloud controllers, we do not have to rely solely on precise design-time knowledge, which may be difficult to acquire. FQL4KE empowers users to specify cloud controllers by simply adjusting weights representing priorities in system goals instead of specifying complex adaptation rules. The applicability of FQL4KE has been experimentally assessed as part of the cloud application framework ElasticBench. The experimental results indicate that FQL4KE outperforms our previously developed fuzzy controller without learning mechanisms and the native Azure auto-scaling.

Maxime Cordy, Patrick Heymans, Pierre-Yves Schobbens et al.

Many product lines are critical, and therefore reliability is a vital part of their requirements. Reliability is a probabilistic property. We therefore propose a model for feature-aware discrete-time Markov chains as a basis for verifying probabilistic properties of product lines, including reliability. We compare three verification techniques: The enumerative technique uses PRISM, a state-of-the-art symbolic probabilistic model checker, on each product. The parametric technique exploits our recent advances in parametric model checking. Finally, we propose a new bounded technique that performs a single bounded verification for the whole product line, and thus takes advantage of the common behaviours of the product line. Experimental results confirm the advantages of the last two techniques.