为推进云计算的发展，本文利用形式化方法对云计算系统的形式语义进行了刻画，并在其基础之上，对云计算中的变化影响分析问题和数据安全性评测问题进行了较为深入地研究，主要工作如下：1）利用抽象源对云计算系统的形式语义进行了刻画。基于在本体中引入动态语义的思想提出了一种新的知识表示方法——抽象源，利用抽象源从云的共性和特性两个角度对云计算系统的形式语义进行了刻画，并通过云服务的一个实例SCSKP对该方法的有效性进行了说明。2）对云计算系统中“变化”的影响进行了分析。构建了一种包含云中“变化”信息的变化传播模型，定义了一种能对该模型进行形式化表示的编码CTMC，并基于变化传播模型和CTMC编码给出了一种可以对云中常见的“变化”影响进行分析的方法。3）利用tabular表达式通用模型对云计算系统进行了描述。在tabular表达式通用模型中扩展了一些新的表类型，给出了一种以抽象源为媒介用tabular表达式对云计算系统进行描述的方法，增强了抽象源的适用性。4）对SCSKP中数据的安全性进行了分析评测。基于SCSKP的抽象源描述分析了SCSKP的安全防护能力，利用马尔可夫模型对SCSKP中各种非法入侵发生的概率进行了分析，基于分析结果计算了非法入侵的损失期望。