SMT-Based Modeling and Verification of Cloud Applications
Cloud applications have been rapidly evolving and gained more and more attention in the past decade. Formal modeling and verification of cloud services are necessarily needed to guarantee their correctness and reliability of complex cloud applications. In this paper, we present a formal framework for modeling and verification of cloud applications based on the SMT solver Z3. Simple cloud services are specified as the basis for the modeling of composition and more complex cloud services. Three different classes Service, Composition and Cloud indicating simple cloud services, composition patterns and composed cloud services are defined, which facilitates the further development of attributes and methods. We also propose an approach to check the refinement and equivalence relations between cloud services, in which counter examples can be automatically generated when the relation is not valid.
KeywordsCloud applications Services Z3 Modeling Verification
The work was partially supported by the National Natural Science Foundation of China under grant no. 61772038 and 61532019.
- 4.Chen, L., Fan, G., Liu, Y.: Modeling and analyzing cost-aware fault tolerant strategy for cloud application. In: Proceedings of SEKE 2016, pp. 439–442. KSI Research Inc. and Knowledge Systems Institute Graduate School (2016)Google Scholar
- 11.Laibinis, L., Byholm, B., Pereverzeva, I., Troubitsyna, E., Eeik Tan, K., Porres, I.: Integrating Event-B modelling and discrete-event simulation to analyse resilience of data stores in the cloud. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 103–119. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_7CrossRefGoogle Scholar
- 12.Nawaz, M.S., Sun, M.: Using PVS for modeling and verifying cloud services and their composition. In: Proceedings of CBD 2018, pp. 42–47. IEEE (2018)Google Scholar
- 13.Reddy, G.S., Feng, Y., Liu, Y., Dong, J.S., Sun, J., Kanagasabai, R.: Towards formal modeling and verification of cloud architectures: a case study on Hadoop. In: Proceedings of SERVICES 2013, pp. 306–311. IEEE Computer Society (2013)Google Scholar
- 16.Sun, M., Fu, G.: A formal design model of cloud services. In: Proceedings of SEKE 2017, pp. 173–178. KSI Research Inc. and Knowledge Systems Institute (2017)Google Scholar