Hypergraphs with constraints was proposed to represent software architectures.The formal semantics and operations of dynamic evolution production rules of software architectures were presented based on hypergraph morphisms.A software architecture style was defined as a type hypergraph,and the dynamic evolution of software architectures was modeled by applying hypergraph grammars and the architecture style.Model checking technique was used to verify the correctness of dynamic evolution of software architectures,an algorithm was designed to verify the property of dynamic evolution of software architectures.Experimental analysis was made by using a model checker.The approach provides a graphical representation of dynamic evolution of software architectures,and displays a formal theoretical framework based on grammars.