research-article

Open access

A verification and deployment approach for elastic component-based applications

Authors:

Mohamed Graiet,

Samir TataAuthors Info & Claims

Formal Aspects of Computing, Volume 29, Issue 6

Pages 987 - 1011

https://doi.org/10.1007/s00165-017-0425-3

Published: 01 November 2017 Publication History

Abstract

Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.

References

References

[1]

Abrial JR Modeling in Event-B: system and software engineering 2010 Cambridge Cambridge University Press

[2]

Albert E, de Boer F-S, Hähnle R, Johnsen E-B, Schlatte R, Tapia Tarifa S-L, and Wong P Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS Serv Oriented Comput Appl 2014 8 4 323-339

Digital Library

[3]

Bersani M-M, Bianculli D, Dustdar S, Gambi A, Ghezzi C, Krstić S (2014) Towards the formalization of properties of cloud-based elastic systems. In: The 6th international workshop on principles of engineering service-oriented and cloud systems. ACM

[4]

Booch G, Rumbaugh J, Jacobson I (2005) Unified modeling language user guide, 2nd edn. Addison-Wesley Professional, Reading

[5]

Chieu T-C, Mohindra A, Karve A-A, Segal A (2009) Dynamic scaling of web applications in a virtualized cloud computing environment. In: The IEEE international conference on e-business engineering. IEEE Computer Society

[6]

Cok D-R (2011) JML for Java 7 by Extending OpenJDK. In: The 3rd international conference on NASA formal methods. Springer

[7]

Calheiros R-N, Vecchiola C, Karunamoorthy D, and Buyya R The Aneka platform and QoS-driven resource provisioning for elastic applications on hybrid clouds Future Gener Comput Syst 2012 28 6 861-870

Digital Library

[8]

Dutta S, Gera S, Akshat V, Viswanathan B (2012) SmartScale: automatic application scaling in enterprise clouds. In: The 5th international conference on cloud computing. IEEE Computer Society

[9]

Dustdar S, Guo Y, Satzger B, and Truong H-L Principles of elastic processes IEEE Internet Comput 2011 15 2 66-71

Digital Library

[10]

Gaaloul G, Bhiri S, and Rouached M Event-based design and runtime verification of composite service transactional behavior IEEE Trans Serv Comput 2010 3 1 32-45

Digital Library

[11]

Galante G, de Bona LCE (2012) A survey on cloud computing elasticity. In: The 5th international conference on utility and cloud computing. IEEE Computer Society

[12]

Geelan J, Klems M, Cohen R, Kaplan J, Gourlay D, Gaw P, Edwards D, De Haaff B, Kepes B, Sheynkman K, Sultan O, Hartig K, Pritzker J, Doerksen T, Von Eicken T, Wallis P, Sheehan M, Dodge D, Ricadela A, Martin B, Kepes B, Berger I-W (2009) Twenty-one experts define cloud computing

[13]

Hamadi R, Benatallah B (2003) A Petri net-based model for web service composition. In: The 14th Australasian database conference. Australian Computer Society

[14]

He S, Guo L, Guo Y, Wu C, Ghanem M, Han R (2012) Elastic application container: a lightweight approach for cloud resource provisioning. In: AINA. IEEE Computer Society

[15]

Hoenisch P, Schulte S, Dustdar S (2013) Workflow scheduling and resource allocation for cloud-based execution of elastic processes. In: The 6th international conference on service-oriented computing and applications. IEEE Computer Society

[16]

Hoenisch P, Schulte S, Dustdar S, Venugopal S (2013) Self-adaptive resource allocation for elastic process execution. In: The 6th international conference on cloud computing. IEEE

[17]

Kranas P, Anagnostopoulos V, Menychtas A, Varvarigou T-A (2012) ElaaS: an innovative elasticity as a service framework for dynamic management across the cloud stack layers. In: The 6th international conference on complex, intelligent, and software intensive systems. IEEE Computer Society

[18]

Klai K, Tata S (2013) Formal modeling of elastic service-based business processes. In: International conference on services computing. IEEE Computer Society

[19]

Leuschel M, Butler M (2003) ProB: a model checker for B. Formal methods, LNCS 2805

[20]

Lahouij A, Hamel L, Graiet M (2013) Formal verification of SCA assembly model with Event-B. In: The 9th international conference on semantics, knowledge and grids. IEEE Computer Society

[21]

Lê L-S, Linh Truong H, Ghose A, Dustdar S (2012) On elasticity and constrainedness of business services provisioning. In: The 9th international conference on services computing. IEEE Computer Society

[22]

Mammar A and Frappier M Proof-based verification approaches for dynamic properties: application to the information system domain Form Asp Comput 2015 27 2 335-374

Digital Library

[23]

Mammar A, Graiet M, Hamel L, Tata S. http://www-public.tem-tsp.eu/~mammar_a/FACElasticity.html

[24]

Mammar A, Graiet M, Hamel L, Tata S (2016) A verification and deployment approach for elastic component-based applications. http://www-public.tem-tsp.eu/~mammar_a/FACElasticity.html

[25]

Marino J, Rowley M (2009) Understanding SCA (Service Component Architecture). Addison-Wesley Professional, Boston

[26]

OASIS (2011) OASIS. Architecture assembly model specification. Version 1.2. 19. http://docs.oasis-open.org/opencsa/sca-assembly/sca-assembly-spec/v1.2/csd01/sca-assembly-spec-v1.2-csd01.html

[27]

Pokahr A and Braubach L Elastic component-based applications in PaaS clouds Concurr Comput Pract Exp 2016 28 4 1368-1384

Digital Library

[28]

Rivera V, Cataño N (2014) Translating Event-B to JML-specified java programs. In: The 29th annual ACM symposium on applied computing. ACM

[29]

Roy N, Dubey A, Gokhale A (2011) Efficient autoscaling in the cloud using predictive models for workload forecasting. In: The 4th international conference on cloud computing. IEEE Computer Society

[30]

Sahli H, Belala F, Bouanaka C (2015) A BRS-based approach to model and verify cloud systems elasticity. In: 1st international conference on cloud forward: from distributed to complete computing

[31]

Solanki M, Cau A, H Zedan H (2006) A wide spectrum language for designing web services. In: The 15th International World Wide Web Conference

[32]

Schulte S, Hoenisch P, Venugopal S, Dustdar S (2013) Introducing the Vienna platform for elastic processes. In: Workshops of international conference on service oriented computing. Springer

[33]

Tsai W-T, Sun X, Shao Q, Qi G (2010) Two-tier multi-tenancy scaling and load balancing. In: The 7th international conference on e-business engineering. IEEE Computer Society

[34]

Vaquero L-M, Rodero-Merino L, and Buyya R Dynamically scaling applications in the cloud SIGCOMM Comput Commun Rev 2011 41 1 45-52

Digital Library

[35]

Yangui S, Ben Nasrallah M, Tata S (2013) PaaS-independent approach to provision appropriate cloud resources for SCA-based applications deployment. In: 9th international conference on semantics, knowledge and grids

[36]

Zhang Q, Cheng L, and Boutaba R Cloud computing: state-of-the-art and research challenges J Internet Serv Appl 2010 1 1 7-18

Cited By

Lahouij AHamel LGraiet M(2023)Formal reconfiguration model for cloud resourcesSoftware and Systems Modeling (SoSyM)10.1007/s10270-022-00990-622:1(225-245)Online publication date: 1-Feb-2023
https://dl.acm.org/doi/10.1007/s10270-022-00990-6
Lahouij AHamel LGraiet M(2022)An Event-B model for dynamically managing cloud resourcesInnovations in Systems and Software Engineering10.1007/s11334-021-00419-118:1(85-104)Online publication date: 1-Mar-2022
https://dl.acm.org/doi/10.1007/s11334-021-00419-1
Lahouij AHamel LGraiet Mel Ayeb B(2020)An Event-B based approach for cloud composite services verificationFormal Aspects of Computing10.1007/s00165-020-00517-032:4-6(361-393)Online publication date: 19-Sep-2020
https://dl.acm.org/doi/10.1007/s00165-020-00517-0
Show More Cited By

Index Terms

A verification and deployment approach for elastic component-based applications
1. General and reference

Index terms have been assigned to the content through auto-classification.

Recommendations

A Formal Approach for Correct Elastic Package-Based Free and Open Source Software Composition in Cloud
On the Move to Meaningful Internet Systems. OTM 2017 Conferences
Abstract
Cloud environments have been increasingly used to deploy and run software while providing a high level performance with a low operating cost. Most of the existing software applications are nowadays distributed as Package-based Free and Open Source ...
A formal approach for the correct deployment of cloud applications
Abstract
The deployment of cloud applications is a complex task. It refers to the enablement of SaaS, PaaS or IaaS solutions that may be accessed on demand by end users. It encompasses all the activities from installation to uninstallation, including ...
Highlights
- This article proposes a generic formal Event-B model for the deployment of correct cloud applications.
- A detailed elicitation of the requirements of cloud applications.
- The proposed approach is illustrated on a case study to prove ...
Is your cloud elastic enough?: performance modelling the elasticity of infrastructure as a service (IaaS) cloud applications
ICPE '12: Proceedings of the 3rd ACM/SPEC International Conference on Performance Engineering

Elasticity, the ability to rapidly scale resources up and down on demand, is an essential feature of public cloud platforms. However, it is difficult to understand the elasticity requirements of a given application and workload, and if the elasticity ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 29, Issue 6

Nov 2017

188 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2017.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2017

Accepted: 01 December 2016

Received: 30 January 2016

Published in FAC Volume 29, Issue 6

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
71
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)8

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lahouij AHamel LGraiet M(2023)Formal reconfiguration model for cloud resourcesSoftware and Systems Modeling (SoSyM)10.1007/s10270-022-00990-622:1(225-245)Online publication date: 1-Feb-2023
https://dl.acm.org/doi/10.1007/s10270-022-00990-6
Lahouij AHamel LGraiet M(2022)An Event-B model for dynamically managing cloud resourcesInnovations in Systems and Software Engineering10.1007/s11334-021-00419-118:1(85-104)Online publication date: 1-Mar-2022
https://dl.acm.org/doi/10.1007/s11334-021-00419-1
Lahouij AHamel LGraiet Mel Ayeb B(2020)An Event-B based approach for cloud composite services verificationFormal Aspects of Computing10.1007/s00165-020-00517-032:4-6(361-393)Online publication date: 19-Sep-2020
https://dl.acm.org/doi/10.1007/s00165-020-00517-0
Lahouij AHamel LGraiet M(2018)Deadlock-Freeness Verification of Cloud Composite Services Using Event-BOn the Move to Meaningful Internet Systems. OTM 2018 Conferences10.1007/978-3-030-02610-3_34(604-622)Online publication date: 22-Oct-2018
https://dl.acm.org/doi/10.1007/978-3-030-02610-3_34

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents