提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.
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.