Chinese Journal of Computers   Full Text
Title	Applying Bigraph Theory to Self-Adaptive Software Architecture
Authors	CHANG Zhi-Ming MAO Xin-Jun QI Zhi-Chang
Address	(School of Computer Science, National University of Defense Technology, Changsha 410073)
Year	2009
Issue	No.1(97—106)
Abstract &   Background	Abstract 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. Keywords Bigraph; BRS; self-adaptive software; software architecture; formalization Background This research is supported by the National Natural Science Foundation of China under grant No.60773018, the National High Technology Research and Development Program (863 Program) of China under grant No.2007AA01Z135, the Postgraduate Innovation Fund of National University of Defense Technology under grant No.070604. These projects aim to build a solid semantic foundation for self-adaptive software, and provide a methodology to validate and check some important properties in the procedure of architectural evolution, such as structural and behavioral consistency and integrity. With the spread of the Internet and software evolution in complex intensive systems, software architecture often need adapt variable environments and design objectives during runtime. To deal with self-adaptive software architectures, the formal method should be presented to describe software architectures and express their changes so that these changes on the evolutions of software architectures could be reasoned about. However, existing theories of mobile and concurrency calculi focus on dynamic software architecture, and can’t provide powerful support for evolutionary properties of self-adaptive software. The theory of Bigraphical reactive systems (BRS), due to Milner and co-workers, is based on a graphical model of mobile computation that emphasizes both locality and connectivity. Informally, a BRS consists of Bigraphs and a set of reaction rules, where Bigraphs can be allowed to reconfigure themselves by reaction rules. Therefore, the theory of BRS can provide a sound concept and intuitive, pervasive expression for self-adaptive software architecture. In this research, the authors used extended BRS as a formal method to describe self-adaptive software architecture. By providing graphic elements and term languages, extended BRS can survey static and dynamic architectures easily. Then they formalized self-adaptive software architecture on structure, behavior and reconfiguration base on extended BRS. By the model based on BRS, they educe a theorem that can ensure architecture consistent, validate the evolving architecture integrity, and check whether the architecture conforms to its style.