摘要

With software systems being more and more open and complex, a major challenge for those systems is to evolve themselves gradually, especially during their runtime, where software architectures can provide a foundation for dynamic software evolution. In this paper, we propose a specifying and verifying method for dynamic evolution of software architectures using hypergraph grammars. We propose two general atomic evolution rules and three general composite evolution rules of software architectures based on hypergraphs, and specify dynamic evolution of software architectures according to those rules and a pre-defined architecture style through a case study. At last we verify the liveness property of dynamic evolution of software architectures using model checking, and give out corresponding verification algorithms. Our approach provides both a user-friendly graphical representation and formal models based on grammars.