中文摘要：

现有的软件体系结构形式化方法对体系结构的动态性、自适应性支持有限，并不能很好地验证系统演化过程中的一致性、完整性等动态特征．Bigraph理论融合了”演算和移动Ambient演算的优势，重点强调计算的位置和连接两方面因素，具有较为完整、可扩展的理论框架．这使得Bigraph不仅在概念上能够满足现有自适应软件对结构和行为的需求，而且还提供了直观、普适的表达能力．文中简要介绍了Bigraph的基本概念和现状，利用Bigraph理论对自适应软件体系结构进行了形式化规约，分析和验证了系统动态演化的性质，并探讨了Bigraph理论在自适应软件体系结构形式化方面的优势和拓展方向．

英文摘要：

Existing theories of mobile and concurrency calculi for dynamic software architecture can not provide powerful support for evolutionary properties of self-adaptive software. Under this circumstance, Bigraph is based on a graphical model of mobile computation that emphasizes both locality and connectivity and has a complete and extensible theory framework. Therefore, Bigraph can provide a sound concept and intuitive, pervasive expression for self-adaptive software architecture. This paper introduces Bigraphical theory and current research, describes self-adaptive software architecture formally, analyzes and verifies some properties of dynamic evolution, and then discusses some promising directions of formal self-adaptive software architecture.