摘要：研究了SOA架构分布式系统在基于社区的Web服务动态会话交互的安全性,提出了一种基于形式化规格说明的Web服务组合行为建模和验证框架.基于OWL-S描述的若干个Web服务的组合和交互的安全性保障问题,构建了一种基于WS-Trust和WS-Secure Conversation规格的安全会话验证方法.该方法首先将Web服务组合行为建模为带有标签的迁移系统AKTS来描述服务的观察行为;进而将安全会话约束翻译为DPDL公式即将SOA系统的会话安全性验证问题规约为保障安全会话约束的前提下的Web服务组合行为的满足性问题;最后通过经典算法在有效时间内得到该满足性问题的验证.该框架为基于SOA架构的分布式系统的交互安全提供了理论支持和保障,在安全关键的分布式系统设计阶段及早发现安全隐患,节约了开发成本、提高了系统安全性.