Formal Analysis of Architectural Policies of Self-Adaptive Software by Bigraph

With the rapid spread of the Internet and user requirements for complex self-adaptive software systems, software often need be reconfigured based on pre-defined or online policies during runtime in open, dynamic environments in order to satisfy design objectives, which poses new problems such as, how to ensure the correction and consistency of the architectural policies? In this paper, we formalize reconfigurable architecture by bigraph, and build automata model for evolution of self-adaptive software architecture. Based on the automata model, we obtain an important theorem for extending the automata, and then present an algorithm which can check the correction and consistency of any self-adaptive software architectural policy.