云计算是伴随互联网的蓬勃发展应运而生的一种新型计算方式，它突破了传统计算的局限，增强了当下急需的计算能力，同时又提供了灵活的可扩展性。云应用是基于云计算思想实现，并部署在云计算环境中的软件系统。云应用大多应用于一些对性能要求很高的领域，因此保障系统的正确性就显得极为关键。本文重点关注云应用与用户、云应用之间和云应用内部的交互正确性。测试和验证是保障软件正确性的主要方法，但是在云环境下，测试技术面临着代价昂贵且操作难度极大等问题。形式化的验证方法规避了上述不足，因而适用于云应用的正确性保障工作。　　基于模型检验的验证工具SPIN能有效地应用于云应用的验证。但是其支持的建模语言PROMELA却难以进行通用直观的建模工作，特别在云应用设计阶段难以体现设计的一般化。SoaML是UML的一种扩展。后者是一种标准建模语言，软件行业的广泛实践已经证明了它在系统建模中的有效性和通用性。SoaML秉承了UML通用直观的特性，同时具备了更高的抽象层次。它弥补了UML没有精确语义和很难描述云应用的不足，可用于云应用的建模。本文首先采用SoaML对云应用进行建模。然后，针对SoaML中的ServiceInterface模型的特点，采用层次自动机来描述ServiceInterface，再根据自动机的语义将其转换为PROMELA。同时，将SoaML中的ServiceContract模型采用线性时序逻辑描述。最后将转换而来的PROMELA和线性时序逻辑公式输入SPIN中就可以进行云应用的自动验证。实验表明，该方法可以有效地验证云应用的正确性。