SMT-Based Modeling and Verification of Cloud Applications

  • Xiyue Zhang
  • Meng SunEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11517)


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.


Cloud applications Services Z3 Modeling Verification 



The work was partially supported by the National Natural Science Foundation of China under grant no. 61772038 and 61532019.


  1. 1.
    Aceto, L., Larsen, K.G., Morichetta, A., Tiezzi, F.: A cost/reward method for optimal infinite scheduling in mobile cloud computing. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 66–85. Springer, Cham (2016). Scholar
  2. 2.
    Alt, L., et al.: HiFrog: SMT-based function summarization for software verification. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 207–213. Springer, Heidelberg (2017). Scholar
  3. 3.
    Benzadri, Z., Belala, F., Bouanaka, C.: Towards a formal model for cloud computing. In: Lomuscio, A.R., Nepal, S., Patrizi, F., Benatallah, B., Brandić, I. (eds.) ICSOC 2013. LNCS, vol. 8377, pp. 381–393. Springer, Cham (2014). Scholar
  4. 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
  5. 5.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). Scholar
  6. 6.
    Fitch, D., Xu, H.: A raid-based secure and fault-tolerant model for cloud information storage. Int. J. Softw. Eng. Knowl. Eng. 23(05), 627–654 (2013)CrossRefGoogle Scholar
  7. 7.
    Freitas, L., Watson, P.: Formalizing workflows partitioning over federated clouds: multi-level security and costs. Int. J. Comput. Math. 91(5), 881–906 (2014)CrossRefGoogle Scholar
  8. 8.
    Graiet, M., Mammar, A., Boubaker, S., Gaaloul, W.: Towards correct cloud resource allocation in business processes. IEEE Trans. Serv. Comput. 10(1), 23–36 (2017)CrossRefGoogle Scholar
  9. 9.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International, Upper Saddle River (1998)zbMATHGoogle Scholar
  10. 10.
    Jifeng, H., Li, X., Liu, Z.: rCOS: a refinement calculus of object systems. Theor. Comput. Sci. 365(1–2), 109–142 (2006)MathSciNetCrossRefGoogle Scholar
  11. 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). Scholar
  12. 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. 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
  14. 14.
    Sim, K.M.: Agent-based cloud computing. IEEE Trans. Serv. Comput. 5(4), 564–577 (2012)CrossRefGoogle Scholar
  15. 15.
    Sun, M., Arbab, F., Aichernig, B.K., Astefanoaei, L., de Boer, F.S., Rutten, J.J.M.M.: Connectors as designs: modeling, refinement and test case generation. Sci. Comput. Program. 77(7–8), 799–822 (2012)zbMATHGoogle Scholar
  16. 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
  17. 17.
    Zhang, P., Lin, C., Ma, X., Ren, F., Li, W.: Monitoring-based task scheduling in large-scale SaaS cloud. In: Sheng, Q.Z., Stroulia, E., Tata, S., Bhiri, S. (eds.) ICSOC 2016. LNCS, vol. 9936, pp. 140–156. Springer, Cham (2016). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Informatics and LMAM, School of Mathematical SciencesPeking UniversityBeijingChina

Personalised recommendations