普适计算通常是在一个动态、异构、开放的物理环境下进行，其中不少物理设备的资源受限、高移动性以及故障频发，这些特征给构建可信的普适服务带来了新的挑战。本文针对普适环境下如何构建可信的普适服务进行研究，从普适服务模型的特征分析着手,提出了一种描述该模型的形式化语言，设计了面向普适应用的类型和效果系统，用于抽取所构建的普适服务的动态行为，进而形式化分析行为一致的服务替换;对于普适服务之间复杂的交互行为进行形式化建模，利用模型检验技术对普适服务的行为属性进行验证；另外还提出了一种普适环境下的动态服务更新框架，以满足复杂动态环境的需求，并抽象出该框架的形式化模型及验证其属性；最后构建了典型的普适应用场景对本文所提出的方法进行验证，实验结果表明该方法的可行性和有效性。本文的主要工作和创新性包括以下几个方面：（1）本文在研究服务构件模型的基础上，着重分析了服务的接口类型和行为语义，并考虑了复杂普适环境下服务实体（设备）的迁移性和可变性，提出了一种普适环境下的服务模型，它具有上下文感知接口、资源访问协议以及可组合性的特征，能够适应普适环境的动态性和满足可信性需求。（2）扩展类型化λ演算以描述服务模型，针对复杂普适环境下服务的组合模式，提出一种面向普适应用的类型和效果系统，运用该系统中的子类型技术来分析行为一致的服务替换，并推导出类型安全性定理。该定理确保了所替换服务的行为是合法的，并且利用Coq辅助证明工具验证了本定理的证明过程是正确的、可信的。（3）利用类型和效果系统技术以抽取出服务的动态行为，将它们转换为相应的服务流程有限状态机；进而可将服务抽象为一种进程模型，利用模型检验工具来自动验证所组合服务的行为属性（例如，安全性、活性），以确认它们符合给定的行为策略，从而确保该服务组合是可信的、有效的。（4）为了适应普适环境的动态性和满足不断变化的用户需求，提出了一种普适环境下的动态服务更新框架，以支持所构建普适应用的在线维护及动态演化。本文定义了该框架的形式化模型，利用模型检验工具来验证其属性（例如，透明性、正确性等），并且证明了动态服务更新也符合类型安全更新的要求；在此基础上，设计出了相应的动态更新系统以支持普适应用的在线更新；该系统不但能够处理动态接口适应性，而且支持更新失败的恢复。实验表明：在更新过程中，该框架给普适应用所造成的性能损失是有限的，并且能够满足动态服务更新的需求。（5）基于OSGi服务平台及支持分布式的R-OSGi中间件技术构建出典型的普适应用场景，以验证本文的理论方法和技术方案的可行性和有效性。