[1] Furht B, Escalante A. Handbook of cloud computing[M]. New York: Springer, 2010.
[2] Mell P, Grance T. The NIST definition of cloud computing[J]. National Institute of Standards and Technology, 2011,53(6):50-57.
[3] Soualhia M, Khomh F, Tahar S. Predicting scheduling failures in the cloud: A case study with google clusters and hadoop on amazon EMR[C]∥2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cyberspace Safety and Security, and 2015 IEEE 12th International Conference on Embedded Software and Systems. Piscataway: IEEE, 2015: 58-65.
[4] Blanchard A, Kosmatov N, Lemerre M, et al. A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C[C]∥International Workshop on Formal Methods for Industrial Critical Systems. Cham:Springer, 2015: 15-30.
[5] Bertot Y, Castéran P. Interactive theorem proving and program development——Coq' Art: The calculus of inductive constructions[M]. Heidelberg: Springer, 2004.
[6] Boubaker S, Gaaloul W, Graiet M, et al. Event-b based approach for verifying cloud resource allocation in business process[C]∥2015 IEEE International Conference on Services Computing. Piscataway: IEEE, 2015: 538-545.
[7] Boubaker S, Mammar A, Graiet M, et al. Formal verification of cloud resource allocation in business processes using Event-B[C]∥2016 IEEE 30th International Conference on Advanced Information Networking and Applications (AINA). Piscataway: IEEE, 2016: 746-753.
[8] Halima R B, Kallel S, Klai K, et al. Formal verification of time-aware cloud resource allocation in business process[C]∥OTM Confederated International Conferences “On the Move to Meaningful Internet Systems”. Cham: Springer, 2016: 400-417.
[9] Singh S, Chana I. Energy based efficient resource scheduling: A step towards green computing[J]. International Journal of Energy, Information and Communications, 2014, 5(2): 35-52.
[10]Chen J, Huang L, Huang H, et al. A formal model for resource protections in web service applications[C]∥2012 International Conference on Cloud and Service Computing. Piscataway:IEEE, 2012: 111-118.
[11]Magee J, Kramer J, Chatley R, et al. LTSA-labelled transition system analyser[EB/OL].[2019-09-03]. http://www.doc.ic.ac.uk/ltsa/, 2012.
[12]Iqbal W, Yousaf S. Formal modeling of agent based cloud computing services using petri nets[J]. VFAST Transactions on Software Engineering, 2013, 1(2): 1-6.
[13]Jlassi S, Mammar A, Abbassi I, et al. Towards correct cloud resource allocation in FOSS applications[J]. Future Generation Computer Systems, 2019, 91: 392-406.
[14]Abrial J R. Modeling in event-B: System and software engineering[M]. Cambridge: Cambridge University Press, 2010.
[15]Keshanchi B, Souri A, Navimipour N J. An improved genetic algorithm for task scheduling in the cloud environments using the priority queues: Formal verification, simulation, and statistical testing[J]. Journal of Systems and Software, 2017, 124: 1-21.
[16]Shen Y, Bao Z, Qin X, et al. Adaptive task scheduling strategy in cloud: When energy consumption meets performance guarantee[J]. World Wide Web, 2017, 20(2): 155-173.
[17]Fan G, Yu H, Chen L, et al. Modeling and analyzing cost and utilization based task scheduling for cloud application[C]∥2016 IEEE 40th Annual Computer Software and Applications Conference (COMPSAC). Piscataway:IEEE, 2016, 1: 245-250.
[18]Abdelsadiq A, Molina-Jimenez C, Shrivastava S. A high-level model-checking tool for verifying service agreements[C]∥Proceedings of 2011 IEEE 6th International Symposium on Service Oriented System (SOSE). Piscataway:IEEE, 2011: 297-304.
[19]Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295.
[20]Kikuchi S, Aoki T. Evaluation of operational vulnerability in cloud service management using model checking[C]∥2013 IEEE Seventh International Symposium on Service-Oriented System Engineering. Piscataway:IEEE, 2013: 37-48.
[21]Kikuchi S, Hiraishi K. Improving reliability in management of cloud computing infrastructure by formal methods[C]∥2014 IEEE Network Operations and Management Symposium (NOMS). Piscataway:IEEE, 2014: 1-7.
[22]Top Threats Working Group. The treacherous 12: Cloud computing top threats in 2016[R]. Cloud Security Alliance, 2016.
[23]Jarraya Y, Eghtesadi A, Debbabi M, et al. Cloud calculus: Security verification in elastic cloud computing platform[C]∥2012 International Conference on Collaboration Technologies and Systems (CTS). Piscataway:IEEE, 2012: 447-454.
[24]Jarraya Y, Eghtesadi A, Debbabi M, et al. Formal verification of security preservation for migrating virtual machines in the cloud[C]∥Symposium on Self-Stabilizing Systems. Berlin, Heidelberg:Springer, 2012: 111-125.
[25]Thuraisingham B, Khadilkar V, Rachapalli J, et al. Towards the design and implementation of a cloud-centric assured information sharing system[R]. Technical Report UTDCS-27-11. The University of Texas at Dallas, 2011.
[26]Kaufmann M, Moore J S. ACL2: An industrial strength version of Nqthm[C]∥Proceedings of 11th Annual Conference on Computer Assurance. COMPASS'96. Piscataway:IEEE, 1996: 23-34.
[27]De Carvalho C A B, De Castro M F, De Castro A R M. Secure cloud storage service for detection of security violations[C]∥Proceedings of the 17th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing. Piscataway:IEEE Press, 2017: 715-718.
[28]Bansal C, Bhargavan K, Delignat-Lavaud A, et al. Keys to the cloud: Formal analysis and concrete attacks on encrypted web storage[C]∥International Conference on Principles of Security and Trust. Berlin, Heidelberg:Springer, 2013: 126-146.
[29]Blanchet B, Abadi M, Fournet C. Automated verification of selected equivalences for security protocols[J]. The Journal of Logic and Algebraic Programming, 2008, 75(1): 3-51.
[30]Rajeb N B, Berrima M, Giraud M, et al. Formal analyze of a private access control protocol to a cloud storage[C]∥14th International Conference on Security and Cryptography (SECRYPT). Setúbal, Portugal: Science and Technology Publications, 2017.
[31]Yu Y, Au M H, Mu Y, et al. Enhanced privacy of a remote data integrity-checking protocol for secure cloud storage[J]. International Journal of Information Security, 2015, 14(4): 307-318.
[32]Yu Y, Zhang Y, Ni J, et al. Remote data possession checking with enhanced security for cloud storage[J]. Future Generation Computer Systems, 2015, 52: 77-85.
[33]Li J, Lin X, Zhang Y, et al. KSF-OABE: Outsourced attribute-based encryption with keyword search function for cloud storage[J]. IEEE Transactions on Services Computing, 2017, 10(5): 715-725.
[34]Chi P W, Lei C L. Audit-free cloud Storage via deniable attribute-based encryption[J]. IEEE Transactions on Cloud Computing, 2018, 6(2): 414-427.
[35]Fan G, Yu H, Chen L, et al. Model based byzantine fault detection technique for cloud computing[C]∥2012 IEEE Asia-Pacific Services Computing Conference.Piscataway: IEEE, 2012: 249-256.
[36]Ren Z, Wang L, Wang Q, et al. Dynamic proofs of retrievability for coded cloud storage systems[J]. IEEE Transactions on Services Computing, 2018, 11(4): 685-698.
[37]Pereverzeva I, Laibinis L, Troubitsyna E, et al. Formal modelling of resilient data storage in cloud[C]∥International Conference on Formal Engineering Methods. Berlin, Heidelberg:Springer, 2013: 363-379.
[38]Camilli M. Petri nets state space analysis in the cloud[C]∥Proceedings of the 34th International Conference on Software Engineering. Piscataway: IEEE Press, 2012: 1638-1640.
[39]Reddy G S, Feng Y, Liu Y, et al. Towards formal modeling and verification of cloud architectures: A case study on hadoop[C]∥2013 IEEE Ninth World Congress on Services. Piscataway:IEEE, 2013: 306-311.
[40]PAT. Process analysis toolkit[EB/OL].[2019-09-03]. http://www.comp.nus.edu.sg/, 2013.
[41]Hao J, Liu Y, Cai W, et al. vTRUST: A formal modeling and verification framework for virtualization systems[C]∥International Conference on Formal Engineering Methods. Berlin, Heidelberg:Springer, 2013: 329-346.
[42]Malik S U R, Khan S U, Srinivasan S K. Modeling and analysis of state-of-the-art VM-based cloud management platforms[J]. IEEE Transactions on Cloud Computing, 2013, 1(1): 50-63.
[43]Barrett C, Ranise S, Stump A, et al. The satisfiability modulo theories library (SMT-LIB)[EB/OL].[2019-09-03]. http://www.smtlib.org/, 2013.
[44]De M L, Bjørner N. Z3: An efficient SMT solver[C]∥International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer, 2008: 337-340.
[45]Kikuchi S, Matsumoto Y. Performance modeling of concurrent live migration operations in cloud computing systems using prism probabilistic model checker[C]∥2011 IEEE 4th International Conference on Cloud Computing. Piscataway: IEEE, 2011: 49-56.
[46]Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic symbolic model checker[C]∥International Conference on Modelling Techniques and Tools for Computer Performance Evaluation. Berlin, Heidelberg:Springer, 2002: 200-204.
[47]Ghosh N, Ghosh S K. An approach to identify and monitor SLA parameters for storage-as-a-service cloud delivery model[C]∥2012 IEEE Globecom Workshops. Piscataway:IEEE, 2012: 724-729.
[48]Hu K, Lei L, Tsai W T. Multi-tenant Verification-as-a-Service (VaaS) in a cloud[J]. Simulation Modelling Practice and Theory, 2016, 60: 122-143.
[49]Freitas L, Watson P. Formalizing workflows partitioning over federated clouds: Multi-level security and costs[J]. International Journal of Computer Mathematics, 2014, 91(5): 881-906.
[50]Woodcock J, Davies J. Using Z: Specification, refinement, and proof[M]. New Jersey:Prentice-Hall, Inc., 1996.
[51]Serbanescu V, Pop F, Cristea V, et al. A formal method for rule analysis and validation in distributed data aggregation service[J]. World Wide Web, 2015, 18(6): 1717-1736.
[52]Liu S, Ölveczky P C, Rahman M R, et al. Formal modeling and analysis of RAMP transaction systems[C]∥Proceedings of the 31st Annual ACM Symposium on Applied Computing. New York: ACM, 2016: 1700-1707.
[53]Bobba R, Grov J, Gupta I, et al. Design, formal modeling, and validation of cloud storage systems using Maude[R]. Technical Report. University of Illinois at Urbana-Champaign, 2017.